pith. machine review for the scientific record. sign in
theorem proved term proof

noble_gas_at_closure

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

formal statement (Lean)

 195theorem noble_gas_at_closure (Z : ℕ) (h : isNobleGas Z) : distToNextClosure Z = 0 := by

proof body

Term-mode proof.

 196  unfold isNobleGas nobleGasZ at h
 197  simp only [List.mem_cons, List.mem_nil_iff, or_false] at h
 198  obtain rfl | rfl | rfl | rfl | rfl | rfl := h <;> native_decide
 199
 200/-- Noble gases have valence electrons equal to their period length (complete shell). -/

used by (2)

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

depends on (8)

Lean names referenced from this declaration's body.