theorem
proved
hadronFamilyCount
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Mathematics.EightFoldWayFromRS on GitHub at line 37.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
34 | pion | kaon | eta | rho | omega
35 deriving DecidableEq, Repr, BEq, Fintype
36
37theorem hadronFamilyCount : Fintype.card HadronFamily = 5 := by decide
38
39structure EightFoldWayCert where
40 octet_2cubeD : mesonOctetCount = 2 ^ 3
41 decuplet_2times5 : baryonDecupletCount = 2 * 5
42 five_families : Fintype.card HadronFamily = 5
43
44def eightFoldWayCert : EightFoldWayCert where
45 octet_2cubeD := mesonOctet_eq_2cubeD
46 decuplet_2times5 := decuplet_eq_2_times_5
47 five_families := hadronFamilyCount
48
49end IndisputableMonolith.Mathematics.EightFoldWayFromRS