def definition def or abbrev

`divConstraint`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 127noncomputable def divConstraint (k : Mode2) (v : VelCoeff) : ℝ :=

Definition body.

 128  (k.1 : ℝ) * v (0 : Fin 2) + (k.2 : ℝ) * v (1 : Fin 2)
 129
 130/-- Fourier-side divergence-free predicate (modewise, at a fixed time). -/

From the project-wide theorem graph. These declarations reference this one in their body.

divConstraint_continuous in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
divConstraint_eq_zero_of_forall in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
divFreeCoeffBound in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
divFree_of_forall in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
IsDivergenceFree in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
IsDivergenceFreeTraj in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
rs_implies_global_regularity_2d_divFreeCoeffBound in IndisputableMonolith.ClassicalBridge.Fluids.Regularity2D decl_use

Lean names referenced from this declaration's body.