theorem
proved
materialClassCount
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.MaterialsScienceFromRS on GitHub at line 26.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
23 | metals | ceramics | polymers | composites | semiconductors
24 deriving DecidableEq, Repr, BEq, Fintype
25
26theorem materialClassCount : Fintype.card MaterialClass = 5 := by decide
27
28/-- Oh group order = 48 = 6 × 2^3. -/
29def ohGroupOrder : ℕ := 48
30theorem ohGroupOrder_eq_6_times_8 : ohGroupOrder = 6 * (2 ^ 3) := by decide
31
32structure MaterialsScienceCert where
33 five_classes : Fintype.card MaterialClass = 5
34 oh_order : ohGroupOrder = 6 * (2 ^ 3)
35
36def materialsScienceCert : MaterialsScienceCert where
37 five_classes := materialClassCount
38 oh_order := ohGroupOrder_eq_6_times_8
39
40end IndisputableMonolith.Physics.MaterialsScienceFromRS