`prefersHCP`

definition

show as: view math explainer →

module: IndisputableMonolith.Chemistry.CrystalStructure
domain: Chemistry
line: 180 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Chemistry.CrystalStructure on GitHub at line 180.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 177def prefersFCC : List ℕ := [29, 47, 79, 13, 28, 82]
 178
 179/-- Metals that prefer HCP: Mg, Zn, Ti, Zr. -/
 180def prefersHCP : List ℕ := [12, 30, 22, 40]
 181
 182/-- Alkali metals prefer BCC (strongest 8-tick coherence). -/
 183theorem alkali_prefer_bcc : ∀ Z, Z ∈ [3, 11, 19, 37, 55] → Z ∈ prefersBCC := by
 184  decide
 185
 186end
 187
 188end CrystalStructure
 189end Chemistry
 190end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.