Documentation

Mathlib.Data.Int.Order.Units

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