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)
20def generationCount : ℕ := 3 -- = D
used by (3)
From the project-wide theorem graph. These declarations reference this one in their body.
-
GenerationCert
in IndisputableMonolith.Physics.ParticlePhysicsGenerationsFromRS
decl_use
-
generations_eq_D
in IndisputableMonolith.Physics.ParticlePhysicsGenerationsFromRS
decl_use
-
totalFermions
in IndisputableMonolith.Physics.ParticlePhysicsGenerationsFromRS
decl_use