def
definition
z8Size
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Mathematics.AbstractHarmoniAnalysisFromRS on GitHub at line 28.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
25theorem lcGroupCount : Fintype.card LCGroup = 5 := by decide
26
27/-- ℤ/8ℤ has 8 elements = 2^3. -/
28def z8Size : ℕ := 8
29theorem z8Size_2cubed : z8Size = 2 ^ 3 := by decide
30
31structure AbstractHarmonicAnalysisCert where
32 five_groups : Fintype.card LCGroup = 5
33 z8_size : z8Size = 2 ^ 3
34
35def abstractHarmonicAnalysisCert : AbstractHarmonicAnalysisCert where
36 five_groups := lcGroupCount
37 z8_size := z8Size_2cubed
38
39end IndisputableMonolith.Mathematics.AbstractHarmonicAnalysisFromRS