inductive
definition
AlgebraicStructure
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Mathematics.AbstractAlgebraFromRS on GitHub at line 22.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
19
20namespace IndisputableMonolith.Mathematics.AbstractAlgebraFromRS
21
22inductive AlgebraicStructure where
23 | group | ring | field | module | algebra
24 deriving DecidableEq, Repr, BEq, Fintype
25
26theorem algebraicStructureCount : Fintype.card AlgebraicStructure = 5 := by decide
27
28/-- |Q₃| = 2^3 = 8 (abelian group). -/
29def q3Size : ℕ := 2 ^ 3
30theorem q3Size_eq_8 : q3Size = 8 := by decide
31
32/-- Q₃ has exponent 2. -/
33def q3Exponent : ℕ := 2
34theorem q3Exponent_eq_2 : q3Exponent = 2 := rfl
35
36structure AbstractAlgebraCert where
37 five_structures : Fintype.card AlgebraicStructure = 5
38 q3_size_8 : q3Size = 8
39 q3_exp_2 : q3Exponent = 2
40
41def abstractAlgebraCert : AbstractAlgebraCert where
42 five_structures := algebraicStructureCount
43 q3_size_8 := q3Size_eq_8
44 q3_exp_2 := q3Exponent_eq_2
45
46end IndisputableMonolith.Mathematics.AbstractAlgebraFromRS