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)
136theorem eight_tick_is_2_cubed : eight_tick = 2^3 := rfl
proof body
Term-mode proof.
137
138/-- If 2^D = 8, then D = 3. -/
depends on (4)
Lean names referenced from this declaration's body.
-
eight_tick
in IndisputableMonolith.Foundation.DimensionForcing
decl_use
-
eight_tick
in IndisputableMonolith.Gap45.PhysicalMotivation
decl_use
-
eight_tick
in IndisputableMonolith.RRF.Foundation.Constants
decl_use
-
eight_tick
in IndisputableMonolith.Thermodynamics.RecognitionThermodynamics
decl_use