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)
51noncomputable def G_N : ℝ := 6.674e-11
proof body
Definition body.
52
53/-- Planck's reduced constant (SI units). -/
used by (16)
From the project-wide theorem graph. These declarations reference this one in their body.
-
area_not_volume
in IndisputableMonolith.Quantum.EntanglementEntropy
decl_use
-
bekensteinHawkingEntropy
in IndisputableMonolith.Quantum.EntanglementEntropy
decl_use
-
bh_entropy_positive
in IndisputableMonolith.Quantum.EntanglementEntropy
decl_use
-
minimalSurfaceArea
in IndisputableMonolith.Quantum.EntanglementEntropy
decl_use
-
planckArea
in IndisputableMonolith.Quantum.EntanglementEntropy
decl_use
-
planckLength
in IndisputableMonolith.Quantum.EntanglementEntropy
decl_use
-
rt_formula_holds
in IndisputableMonolith.Quantum.EntanglementEntropy
decl_use
-
ryuTakayanagi
in IndisputableMonolith.Quantum.EntanglementEntropy
decl_use
-
AdSCFT
in IndisputableMonolith.Quantum.HolographicBound
decl_use
-
dynamicalTime
in IndisputableMonolith.Unification.BandwidthSaturation
decl_use
-
gravArea
in IndisputableMonolith.Unification.BandwidthSaturation
decl_use
-
gravArea_inv_sq
in IndisputableMonolith.Unification.BandwidthSaturation
decl_use
-
gravArea_pos
in IndisputableMonolith.Unification.BandwidthSaturation
decl_use
-
high_accel_newtonian
in IndisputableMonolith.Unification.BandwidthSaturation
decl_use
-
low_accel_saturated
in IndisputableMonolith.Unification.BandwidthSaturation
decl_use
-
newtonAccel
in IndisputableMonolith.Unification.BandwidthSaturation
decl_use
depends on (1)
Lean names referenced from this declaration's body.
-
constant
in IndisputableMonolith.Relativity.Fields.Scalar
decl_use