# Documentation

Mathlib.Data.Int.Units

# Lemmas about units in ℤ. #

### units #

@[simp]
theorem Int.units_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 : ) (hu' : IsUnit u') :
u u' u = -u'
theorem Int.isUnit_eq_one_or {a : } :
a = 1 a = -1
theorem Int.isUnit_iff {a : } :
a = 1 a = -1
theorem Int.isUnit_eq_or_eq_neg {a : } {b : } (ha : ) (hb : ) :
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 : } :
= 1

Alias of the forward direction of Int.isUnit_iff_natAbs_eq.

theorem Int.ofNat_isUnit {n : } :
IsUnit n
theorem Int.isUnit_mul_self {a : } (ha : ) :
a * a = 1
theorem Int.isUnit_add_isUnit_eq_isUnit_add_isUnit {a : } {b : } {c : } {d : } (ha : ) (hb : ) (hc : ) (hd : ) :
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