mathlib3 documentation

data.int.order.units

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 : ˣ) :
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)