Units in the integers

Units

theorem Int.units_natAbs (u : ℤˣ) : (↑u).natAbs = 1

@[simp]

theorem Int.natAbs_of_isUnit {u : ℤ} (hu : IsUnit u) : u.natAbs = 1

theorem Int.isUnit_eq_one_or {u : ℤ} (hu : IsUnit u) : u = 1 ∨ u = -1

theorem Int.isUnit_ne_iff_eq_neg {u v : ℤ} (hu : IsUnit u) (hv : IsUnit v) : u ≠ v ↔ u = -v

theorem Int.isUnit_eq_or_eq_neg {u v : ℤ} (hu : IsUnit u) (hv : IsUnit v) : u = v ∨ u = -v

theorem Int.isUnit_iff {u : ℤ} : IsUnit u ↔ u = 1 ∨ u = -1

theorem Int.eq_one_or_neg_one_of_mul_eq_one {u v : ℤ} (h : u * v = 1) : u = 1 ∨ u = -1

theorem Int.eq_one_or_neg_one_of_mul_eq_one' {u v : ℤ} (h : u * v = 1) : u = 1 ∧ v = 1 ∨ u = -1 ∧ v = -1

theorem Int.eq_of_mul_eq_one {u v : ℤ} (h : u * v = 1) : u = v

theorem Int.mul_eq_one_iff_eq_one_or_neg_one {u v : ℤ} : u * v = 1 ↔ u = 1 ∧ v = 1 ∨ u = -1 ∧ v = -1

theorem Int.eq_one_or_neg_one_of_mul_eq_neg_one' {u v : ℤ} (h : u * v = -1) : u = 1 ∧ v = -1 ∨ u = -1 ∧ v = 1

theorem Int.mul_eq_neg_one_iff_eq_one_or_neg_one {u v : ℤ} : u * v = -1 ↔ u = 1 ∧ v = -1 ∨ u = -1 ∧ v = 1

theorem Int.isUnit_iff_natAbs_eq {u : ℤ} : IsUnit u ↔ u.natAbs = 1

theorem Int.IsUnit.natAbs_eq {u : ℤ} : IsUnit u → u.natAbs = 1

Alias of the forward direction of Int.isUnit_iff_natAbs_eq.

theorem Int.ofNat_isUnit {n : ℕ} : IsUnit ↑n ↔ IsUnit n

theorem Int.isUnit_mul_self {u : ℤ} (hu : IsUnit u) : u * u = 1

theorem Int.isUnit_add_isUnit_eq_isUnit_add_isUnit {a b c d : ℤ} (ha : IsUnit a) (hb : IsUnit b) (hc : IsUnit c) (hd : IsUnit d) : a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c

theorem Int.eq_one_or_neg_one_of_mul_eq_neg_one {u v : ℤ} (h : u * v = -1) : u = 1 ∨ u = -1