Basic lemmas for ℤˣ.

This file contains lemmas on the units of ℤ.

Main results

• Int.units_eq_one_or: the invertible integers are 1 and -1.

See note [foundational algebra order theory].

Units

theorem Int.units_eq_one_or (u : Units Int) : Or (Eq u 1) (Eq u (-1))

theorem Int.units_ne_iff_eq_neg {u v : Units Int} : Iff (Ne u v) (Eq u (Neg.neg v))