Unity_and_Negative_form_Subgroup_of_Units
Provedproofwikiringssubgroupsunits
Let R be a ring with unity. Then {1, -1} forms a subgroup of the group of units.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Unity_and_Negative_form_Subgroup_of_Units {R : Type _} [Ring R] : IsUnit (1 : R) ∧ IsUnit ((-1 : R)) := by sorrySource