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 : ℤˣ) : u = 1 ∨ u = -1

theorem Int.units_ne_iff_eq_neg {u : ℤˣ} {v : ℤˣ} : u ≠ v ↔ u = -v