Lemmas about units in ℤ.

units

@[simp]

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

theorem Int.units_eq_one_or (u : ℤˣ) : u = 1 ∨ u = -1

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

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

theorem Int.isUnit_eq_one_or {a : ℤ} : IsUnit a → a = 1 ∨ a = -1

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

theorem Int.isUnit_eq_or_eq_neg {a : ℤ} {b : ℤ} (ha : IsUnit a) (hb : IsUnit b) : a = b ∨ a = -b

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

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

theorem Int.eq_of_mul_eq_one {z : ℤ} {w : ℤ} (h : z * w = 1) : z = w

theorem Int.mul_eq_one_iff_eq_one_or_neg_one {z : ℤ} {w : ℤ} : z * w = 1 ↔ z = 1 ∧ w = 1 ∨ z = -1 ∧ w = -1

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

theorem Int.mul_eq_neg_one_iff_eq_one_or_neg_one {z : ℤ} {w : ℤ} : z * w = -1 ↔ z = 1 ∧ w = -1 ∨ z = -1 ∧ w = 1

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

theorem Int.IsUnit.natAbs_eq {n : ℤ} : IsUnit n → Int.natAbs n = 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 {a : ℤ} (ha : IsUnit a) : a * a = 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 {z : ℤ} {w : ℤ} (h : z * w = -1) : z = 1 ∨ z = -1