theorem
other
other
smSectorCount
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)
30theorem smSectorCount : Fintype.card SMLagrangianSector = 5 := by decide
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
-
smLagrangianCert
in IndisputableMonolith.Physics.StandardModelLagrangianStructure
decl_use
depends on (2)
Lean names referenced from this declaration's body.
-
SMLagrangianSector
in IndisputableMonolith.Foundation.QRFT.SMLagrangianSkeleton
decl_use
-
SMLagrangianSector
in IndisputableMonolith.Physics.StandardModelLagrangianStructure
decl_use