Skip to main content

Source-pinned research

Research proof index

Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.

This index contains 2,569 curated research declarations and 119,070 complete package declarations. Search 10,000 more complete Mathlib declarations.

All topics

Showing 1,135 to 1,140 of 2,569 results.

Project-declaredLean 4.32.0

Cauchy Momentum Equation iff convective Cauchy Momentum Equation

FluidDynamics.CauchyFlow.cauchyMomentumEquation_iff_convectiveCauchyMomentumEquation

Mathematical statement

The conservative and convective Cauchy momentum equations are equivalent when the classical continuity equation holds. The differentiability assumptions are exactly the product-rule assumptions used to rewrite partial_t (rho u) and matrixDiv (rho u ⊗ u).

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Euler iff convective Euler

FluidDynamics.euler_iff_convectiveEuler

Mathematical statement

The conservative and convective Euler forms are equivalent when the fields are differentiable enough for the product rules.

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Matrix Div momentum Flux

FluidDynamics.FluidFlow.matrixDiv_momentumFlux

Mathematical statement

The matrix divergence of rho u ⊗ u split into continuity and convective parts.

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Space Deriv momentum Flux component

FluidDynamics.FluidFlow.spaceDeriv_momentumFlux_component

Mathematical statement

Product rule for one spatial derivative of one component of rho u ⊗ u.

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Time Deriv smul velocity

FluidDynamics.FluidFlow.timeDeriv_smul_velocity

Mathematical statement

Product rule for the time derivative of a scalar field times a velocity field.

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record