mathlib3 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 #

source
@[simp]
theorem int.units_nat_abs (u : ℤˣ) :
↑u.nat_abs = 1
source
theorem int.units_eq_one_or (u : ℤˣ) :
u = 1 ∨ u = -1
source
theorem int.is_unit_eq_one_or {a : ℤ} :
is_unit a → a = 1 ∨ a = -1
source
theorem int.is_unit_iff {a : ℤ} :
is_unit a ↔ a = 1 ∨ a = -1
source
theorem int.is_unit_eq_or_eq_neg {a b : ℤ} (ha : is_unit a) (hb : is_unit b) :
a = b ∨ a = -b
source
theorem int.eq_one_or_neg_one_of_mul_eq_one {z w : ℤ} (h : z * w = 1) :
z = 1 ∨ z = -1
source
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
source
theorem int.eq_of_mul_eq_one {z w : ℤ} (h : z * w = 1) :
z = w
source
theorem int.mul_eq_one_iff_eq_one_or_neg_one {z w : ℤ} :
z * w = 1 ↔ z = 1 ∧ w = 1 ∨ z = -1 ∧ w = -1
source
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
source
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
source
theorem int.is_unit_iff_nat_abs_eq {n : ℤ} :
is_unit n ↔ n.nat_abs = 1
source
theorem int.is_unit.nat_abs_eq {n : ℤ} :
is_unit n → n.nat_abs = 1

Alias of the forward direction of int.is_unit_iff_nat_abs_eq.

source
@[norm_cast]
theorem int.of_nat_is_unit {n : ℕ} :
is_unit ↑n ↔ is_unit n
source
theorem int.is_unit_mul_self {a : ℤ} (ha : is_unit a) :
a * a = 1
source
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
source
theorem int.eq_one_or_neg_one_of_mul_eq_neg_one {z w : ℤ} (h : z * w = -1) :
z = 1 ∨ z = -1