structure
definition
CrystalSystemsCert
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 38.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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