def
definition
def or abbrev
rho_lambda_observed
show as:
view Lean formalization →
formal statement (Lean)
46noncomputable def rho_lambda_observed : ℝ := 6e-27
proof body
Definition body.
47
48/-- The dark energy scale in eV: (ρ_Λ c² / ℏ³ c³)^(1/4) ≈ 2 meV. -/