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)
295inductive CellDim where
296 | vertex : CellDim
297 | edge : CellDim
298 | face : CellDim
299 | cube : CellDim
300deriving DecidableEq
301
302/-- Number of k-cells in the 3-cube. -/
used by (4)
From the project-wide theorem graph. These declarations reference this one in their body.
-
anchorsPerCell
in IndisputableMonolith.Physics.LeptonGenerations.TauStepDeltaDerivation
decl_use
-
cellCount
in IndisputableMonolith.Physics.LeptonGenerations.TauStepDeltaDerivation
decl_use
-
localCoeff
in IndisputableMonolith.Physics.LeptonGenerations.TauStepDeltaDerivation
decl_use
-
localCoeff_eq_three_halves_iff
in IndisputableMonolith.Physics.LeptonGenerations.TauStepDeltaDerivation
decl_use
depends on (5)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use