Documentation

Mathlib.Data.Int.Units

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
@[simp]
theorem Int.units_ne_neg_self (u : ˣ) :
u -u
@[simp]
theorem Int.neg_units_ne_self (u : ˣ) :
-u u
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 aa = 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.natAbs_eq {n : } :
IsUnit nInt.natAbs n = 1

Alias of the forward direction of Int.isUnit_iff_natAbs_eq.

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