Lemmas about units in `ℤ`, which interact with the order structure. #

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

theorem int.is_unit_iff_abs_eq {x : ℤ} :

theorem int.is_unit_sq {a : ℤ} (ha : is_unit a) :

a ^ 2 = 1

@[simp]

theorem int.units_sq (u : ℤ ˣ) :

u ^ 2 = 1

theorem int.units_pow_two (u : ℤ ˣ) :

u ^ 2 = 1

Alias of int.units_sq.

@[simp]

theorem int.units_mul_self (u : ℤ ˣ) :

u * u = 1

@[simp]

theorem int.units_inv_eq_self (u : ℤ ˣ) :

@[simp]

theorem int.units_coe_mul_self (u : ℤ ˣ) :

@[simp]

theorem int.neg_one_pow_ne_zero {n : ℕ} :

(-1) ^ n ≠ 0

theorem int.sq_eq_one_of_sq_lt_four {x : ℤ} (h1 : x ^ 2 < 4) (h2 : x ≠ 0) :

x ^ 2 = 1

theorem int.sq_eq_one_of_sq_le_three {x : ℤ} (h1 : x ^ 2 ≤ 3) (h2 : x ≠ 0) :

x ^ 2 = 1

theorem int.units_pow_eq_pow_mod_two (u : ℤ ˣ) (n : ℕ) :

u ^ n = u ^ (n % 2)

Lemmas about units in ℤ, which interact with the order structure. #