No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
47noncomputable def planckEnergy : ℝ := planckMass * c^2
proof body
Definition body.
48
49/-- The Planck temperature T_P = E_P / k_B ≈ 1.417 × 10³² K. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (9)
Lean names referenced from this declaration's body.
-
K
in IndisputableMonolith.Constants
decl_use
-
K
in IndisputableMonolith.Constants.LambdaRecDerivation
decl_use
-
k_B
in IndisputableMonolith.Information.ComputationLimitsStructure
decl_use
-
k_B
in IndisputableMonolith.Quantum.BekensteinHawking
decl_use
-
planckMass
in IndisputableMonolith.Quantum.BekensteinHawking
decl_use
-
k_B
in IndisputableMonolith.Quantum.PageCurve
decl_use
-
planckMass
in IndisputableMonolith.Quantum.PlanckScale
decl_use
-
temperature
in IndisputableMonolith.Thermodynamics.BoltzmannDistribution
decl_use
-
k_B
in IndisputableMonolith.Thermodynamics.PartitionFunction
decl_use