mathlib documentation

data.int.units

Lemmas about units in . #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

units #

@[simp]
theorem int.units_nat_abs (u : ˣ) :
theorem int.units_eq_one_or (u : ˣ) :
u = 1 u = -1
theorem int.is_unit_eq_one_or {a : } :
is_unit a a = 1 a = -1
theorem int.is_unit_iff {a : } :
is_unit a a = 1 a = -1
theorem int.is_unit_eq_or_eq_neg {a b : } (ha : is_unit a) (hb : is_unit 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.is_unit.nat_abs_eq {n : } :

Alias of the forward direction of int.is_unit_iff_nat_abs_eq.

@[norm_cast]
theorem int.is_unit_mul_self {a : } (ha : is_unit a) :
a * a = 1
theorem int.is_unit_add_is_unit_eq_is_unit_add_is_unit {a b c d : } (ha : is_unit a) (hb : is_unit b) (hc : is_unit c) (hd : is_unit 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