Mathlib.Algebra.Ring.Int.Units

Module docstring

{"# Basic lemmas for ℤˣ.

This file contains lemmas on the units of ℤ.

Main results

See note [foundational algebra order theory]. ","#### Units "}

Int.units_eq_one_or theorem

(u : ℤˣ) : u = 1 ∨ u = -1

Full source

lemma units_eq_one_or (u : ℤℤˣ) : u = 1 ∨ u = -1 := by
  simpa only [Units.ext_iff] using isUnit_eq_one_or u.isUnit

Units of Integers are $\pm 1$

Informal description

For any unit $u$ in the group of units of the integers $\mathbb{Z}^\times$, either $u = 1$ or $u = -1$.

Int.units_ne_iff_eq_neg theorem

{u v : ℤˣ} : u ≠ v ↔ u = -v

Full source

lemma units_ne_iff_eq_neg {u v : ℤℤˣ} : u ≠ vu ≠ v ↔ u = -v := by
  simpa only [Ne, Units.ext_iff] using isUnit_ne_iff_eq_neg u.isUnit v.isUnit

Units in $\mathbb{Z}^\times$ are distinct if and only if they are negatives

Informal description

For any two units $u$ and $v$ in the group of invertible integers $\mathbb{Z}^\times$, we have $u \neq v$ if and only if $u = -v$.