def definition def or abbrev

`superfluid_fraction`

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

formal statement (Lean)

 117noncomputable def superfluid_fraction (T Tlam : ℝ) : ℝ :=

Definition body.

 118  1 - (T / Tlam) ^ rs_critical_exponent
 119
 120/-- At T = 0, fully superfluid. -/

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

superfluid_fraction_at_lambda in IndisputableMonolith.Physics.Superfluidity decl_use
superfluid_fraction_at_zero in IndisputableMonolith.Physics.Superfluidity decl_use
superfluid_fraction_between in IndisputableMonolith.Physics.Superfluidity decl_use

Lean names referenced from this declaration's body.