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)
31def rankSU2 : ℕ := 2
used by (7)
From the project-wide theorem graph. These declarations reference this one in their body.
-
ElectroweakCert
in IndisputableMonolith.Physics.ElectrowealUnificationFromRS
decl_use
-
ew_from_su2_u1
in IndisputableMonolith.Physics.ElectrowealUnificationFromRS
decl_use
-
rankEW
in IndisputableMonolith.Physics.ElectrowealUnificationFromRS
decl_use
-
rankSU2
in IndisputableMonolith.Physics.ElectrowealUnificationFromRS
decl_use
-
SMGroupCert
in IndisputableMonolith.Physics.StandardModelGroupStructure
decl_use
-
totalRank
in IndisputableMonolith.Physics.StandardModelGroupStructure
decl_use
-
wBosonCount
in IndisputableMonolith.Physics.StandardModelGroupStructure
decl_use
depends on (1)
Lean names referenced from this declaration's body.
-
rankSU2
in IndisputableMonolith.Physics.ElectrowealUnificationFromRS
decl_use