module module

`IndisputableMonolith.Chemistry.AtomicRadii`

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.Electronegativity module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Chemistry.PeriodicTable module_import
IndisputableMonolith.Constants module_import

declarations in this module (28)

def shellNumber L33
def shellRadiusProxy L37
def screeningFactor L42
def radiusProxy L48
def normalizedRadius L53
theorem lower_z_more_remaining L63
theorem shell_radius_increases_with_period L75
theorem li_valence_one L87
theorem na_valence_one L88
theorem k_valence_one L89
theorem rb_valence_one L90
theorem cs_valence_one L91
theorem fr_valence_one L92
theorem f_dist_one L95
theorem cl_dist_one L96
theorem br_dist_one L97
theorem i_dist_one L98
theorem at_dist_one L99
theorem helium_full_shell L102
theorem neon_full_shell L103
theorem argon_full_shell L104
theorem krypton_full_shell L105
theorem xenon_full_shell L106
theorem radon_full_shell L107
theorem oganesson_full_shell L108
theorem li_larger_than_f L115
theorem na_larger_than_cl L122
theorem k_larger_shell_than_li L127