structure
definition
ConwayCert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Mathematics.ConwayGroupStructuralFromRS on GitHub at line 32.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
29/-- 24 = 2³ · 3 (integer factorisation). -/
30theorem leechDim_factorisation : leechDimension = 2 ^ 3 * 3 := by decide
31
32structure ConwayCert where
33 leech_dim : leechDimension = 24
34 leech_half_b3 : leechFromCube = leechDimension
35 leech_factorisation : leechDimension = 2 ^ 3 * 3
36
37def conwayCert : ConwayCert where
38 leech_dim := leechDimension_eq
39 leech_half_b3 := leech_half_b3
40 leech_factorisation := leechDim_factorisation
41
42end IndisputableMonolith.Mathematics.ConwayGroupStructuralFromRS