def
definition
def or abbrev
E_coh
show as:
view Lean formalization →
formal statement (Lean)
133noncomputable def E_coh : ℝ := Constants.phi ^ (-(coherence_exponent : ℤ))
proof body
Definition body.
134
135/-- E_coh = φ^{-5} -/