structure
definition
EightFoldWayCert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Mathematics.EightFoldWayFromRS on GitHub at line 39.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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