theorem
proved
generationTypeCount
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.ParticlePhysicsGenerationsFromRS on GitHub at line 36.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
33 | first | second | third
34 deriving DecidableEq, Repr, BEq, Fintype
35
36theorem generationTypeCount : Fintype.card FermionGeneration = 3 := by decide
37
38structure GenerationCert where
39 three_generations : generationCount = 3
40 total_12 : totalFermions = 12
41 cube_edge_match : totalFermions = cubeEdges
42 generation_types : Fintype.card FermionGeneration = 3
43
44def generationCert : GenerationCert where
45 three_generations := generations_eq_D
46 total_12 := total_fermions_eq_12
47 cube_edge_match := total_fermions_eq_cube_edges
48 generation_types := generationTypeCount
49
50end IndisputableMonolith.Physics.ParticlePhysicsGenerationsFromRS