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

theorem Int.isUnit_iff_abs_eq {x : ℤ} : IsUnit x ↔ |x| = 1

theorem Int.isUnit_sq {a : ℤ} (ha : IsUnit 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 : ℤˣ) : u⁻¹ = u

@[simp]

theorem Int.units_coe_mul_self (u : ℤˣ) : ↑u * ↑u = 1

@[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)