def definition def or abbrev

`circulatingPart`

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

formal statement (Lean)

  22def circulatingPart {ι : Type*} (X : NESSVectorField ι) : ι → ℝ :=

Definition body.

  23  fun i => X.v i + X.freeEnergyGradient i
  24

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

HelmholtzDecompositionCert in IndisputableMonolith.Information.HelmholtzDecomposition decl_use
helmholtz_split in IndisputableMonolith.Information.HelmholtzDecomposition decl_use

Lean names referenced from this declaration's body.

NESSVectorField in IndisputableMonolith.Information.HelmholtzDecomposition decl_use