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

halogen_ea_one

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)

  67theorem halogen_ea_one (Z : ℕ) (h : isHalogen Z) : eaProxy Z = 1 := by

proof body

Term-mode proof.

  68  simp only [eaProxy, distToClosure]
  69  exact h
  70
  71/-- Fluorine is a halogen (in list). -/

depends on (10)

Lean names referenced from this declaration's body.