module module

`IndisputableMonolith.Chemistry.Electronegativity`

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

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Chemistry.IonicBond module_import

depends on (4)

Lean names referenced from this declaration's body.

IndisputableMonolith.Chemistry.AtomicRadii module_import
IndisputableMonolith.Chemistry.ElectronAffinity module_import
IndisputableMonolith.Chemistry.PeriodicTable module_import
IndisputableMonolith.Constants module_import

declarations in this module (18)

def enProxy L36
def enRanking L43
theorem fluorine_gt_li L50
theorem fluorine_gt_be L54
theorem fluorine_gt_b L58
theorem fluorine_gt_c L62
theorem fluorine_gt_n L66
theorem fluorine_gt_o L70
theorem chlorine_gt_sodium L74
theorem en_increases_across_period L79
theorem group_17_en_order L92
theorem alkali_min_valence L97
theorem cesium_low_en L104
theorem carbon_intermediate L109
theorem nitrogen_ranking L114
theorem oxygen_ranking L119
theorem fluorine_ranking L124
theorem noble_gas_zero_en L131