inductive
definition
LCGroup
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Mathematics.AbstractHarmonicAnalysisFromRS on GitHub at line 21.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
18
19namespace IndisputableMonolith.Mathematics.AbstractHarmonicAnalysisFromRS
20
21inductive LCGroup where
22 | real | integer | circle | pAdic | generalLinear
23 deriving DecidableEq, Repr, BEq, Fintype
24
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