theorem
proved
orthogonalSystem_count
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.CrystalSystemsFromConfigDim on GitHub at line 28.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
25 | hexagonal
26 deriving DecidableEq, Repr, BEq, Fintype
27
28theorem orthogonalSystem_count :
29 Fintype.card OrthogonalCrystalSystem = 5 := by decide
30
31/-- 7 systems total; 5 orthogonal + 2 oblique. -/
32theorem seven_systems_partition : (7 : ℕ) = 5 + 2 := by decide
33
34/-- 14 Bravais lattices. -/
35def bravaisLatticeCount : ℕ := 14
36theorem bravais_eq : bravaisLatticeCount = 14 := rfl
37
38structure CrystalSystemsCert where
39 five_orthogonal : Fintype.card OrthogonalCrystalSystem = 5
40 seven_total : (7 : ℕ) = 5 + 2
41 bravais_14 : bravaisLatticeCount = 14
42
43def crystalSystemsCert : CrystalSystemsCert where
44 five_orthogonal := orthogonalSystem_count
45 seven_total := seven_systems_partition
46 bravais_14 := bravais_eq
47
48end IndisputableMonolith.Physics.CrystalSystemsFromConfigDim