def definition def or abbrev

`ell0`

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

formal statement (Lean)

  71def ell0 : ℝ := c_codata * tau0

proof body

Definition body.

used by (40)

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

BridgeData in IndisputableMonolith.Bridge.DataCore decl_use
computeRatios in IndisputableMonolith.Certificates.UnitsKGate decl_use
UnitsKGateCert in IndisputableMonolith.Certificates.UnitsKGate decl_use
c_ell0_tau0 in IndisputableMonolith.Constants decl_use
E_coh_pos in IndisputableMonolith.Constants decl_use
ell0 in IndisputableMonolith.Constants decl_use
ell0_pos in IndisputableMonolith.Constants decl_use
kappa_einstein_eq in IndisputableMonolith.Constants decl_use
lambda_rec in IndisputableMonolith.Constants decl_use
RSUnits in IndisputableMonolith.Constants decl_use
canonicalUnits in IndisputableMonolith.Constants.Derivation decl_use
ell0_ne_zero in IndisputableMonolith.Constants.Derivation decl_use
ell0_pos in IndisputableMonolith.Constants.Derivation decl_use
units_self_consistent in IndisputableMonolith.Constants.Derivation decl_use
display_rate_matches_structural_rate in IndisputableMonolith.Constants.KDisplay decl_use
displays_invariant_under_equivalence in IndisputableMonolith.Constants.KDisplay decl_use
ell0_div_tau0_eq_c in IndisputableMonolith.Constants.KDisplay decl_use
K_gate_check in IndisputableMonolith.Constants.KDisplay decl_use
KGateMeasurement in IndisputableMonolith.Constants.KDisplay decl_use
K_gate_units_invariant in IndisputableMonolith.Constants.KDisplay decl_use
observable_factors_through_quotient in IndisputableMonolith.Constants.KDisplay decl_use
single_inequality_audit in IndisputableMonolith.Constants.KDisplay decl_use
UnitsEquivalent in IndisputableMonolith.Constants.KDisplay decl_use
UnitsEquivalent in IndisputableMonolith.Constants.KDisplay decl_use
UnitsEquivalent in IndisputableMonolith.Constants.KDisplay decl_use
units_quotient_preserves_K in IndisputableMonolith.Constants.KDisplay decl_use
K_gate_eqK in IndisputableMonolith.Constants.KDisplayCore decl_use
lambda_kin_display in IndisputableMonolith.Constants.KDisplayCore decl_use
lambda_kin_display_ratio in IndisputableMonolith.Constants.KDisplayCore decl_use
lambda_kin_from_tau_rec in IndisputableMonolith.Constants.KDisplayCore decl_use

… and 10 more

depends on (5)

Lean names referenced from this declaration's body.

tau0 in IndisputableMonolith.Compat.Constants decl_use
ell0 in IndisputableMonolith.Constants decl_use
tau0 in IndisputableMonolith.Constants decl_use
c_codata in IndisputableMonolith.Constants.Derivation decl_use
tau0 in IndisputableMonolith.Constants.Derivation decl_use