module module

`IndisputableMonolith.Chemistry.MetallicBond`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Chemistry.PeriodicTable module_import
IndisputableMonolith.Constants module_import

declarations in this module (17)

def transitionMetalZ L34
def alkaliMetalZ L43
def alkalineEarthZ L46
def isMetal L49
def freeElectrons L58
def conductivityProxy L69
inductive LatticeType L74
def coordinationNumber L81
def packingEfficiency L87
theorem bcc_8tick L93
theorem close_packed_12 L96
theorem fcc_hcp_denser_than_bcc L100
theorem alkali_low_ionization L106
def cohesiveEnergyProxy L115
theorem transition_cohesive_gt_alkali L122
def lorenzNumber L161
theorem lorenz_positive L165