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

theorem Int.isUnit_iff_abs_eq {x : Int} : Iff (IsUnit x) (Eq (abs x) 1)

theorem Int.isUnit_sq {a : Int} (ha : IsUnit a) : Eq (HPow.hPow a 2) 1

theorem Int.units_sq (u : Units Int) : Eq (HPow.hPow u 2) 1

theorem Int.units_pow_two (u : Units Int) : Eq (HPow.hPow u 2) 1

Alias of Int.units_sq.

theorem Int.units_mul_self (u : Units Int) : Eq (HMul.hMul u u) 1

theorem Int.units_inv_eq_self (u : Units Int) : Eq (Inv.inv u) u

theorem Int.units_div_eq_mul (u₁ u₂ : Units Int) : Eq (HDiv.hDiv u₁ u₂) (HMul.hMul u₁ u₂)

theorem Int.units_coe_mul_self (u : Units Int) : Eq (HMul.hMul u.val u.val) 1

theorem Int.neg_one_pow_ne_zero {n : Nat} : Ne (HPow.hPow (-1) n) 0

theorem Int.sq_eq_one_of_sq_lt_four {x : Int} (h1 : LT.lt (HPow.hPow x 2) 4) (h2 : Ne x 0) : Eq (HPow.hPow x 2) 1

theorem Int.sq_eq_one_of_sq_le_three {x : Int} (h1 : LE.le (HPow.hPow x 2) 3) (h2 : Ne x 0) : Eq (HPow.hPow x 2) 1

theorem Int.units_pow_eq_pow_mod_two (u : Units Int) (n : Nat) : Eq (HPow.hPow u n) (HPow.hPow u (HMod.hMod n 2))