inductive definition def or abbrev

`Centering`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 130inductive Centering
 131| P  -- Primitive
 132| I  -- Body-centered
 133| F  -- Face-centered
 134| A  -- A-face centered
 135| B  -- B-face centered
 136| C  -- C-face centered
 137| R  -- Rhombohedral
 138deriving DecidableEq, Repr
 139
 140/-- Number of Bravais lattices per crystal system. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

point_groups_sum in IndisputableMonolith.Chemistry.CrystalSymmetry decl_use

depends on (13)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
Primitive in IndisputableMonolith.Ethics.Virtues.NormalForm decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
Primitive in IndisputableMonolith.Masses.SectorPrimitive decl_use
A in IndisputableMonolith.Modal.Actualization decl_use
F in IndisputableMonolith.Physics.AnchorPolicy decl_use
F in IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation decl_use
F in IndisputableMonolith.Pipelines decl_use