Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
```/-

! This file was ported from Lean 3 source module data.int.order.units
! leanprover-community/mathlib commit d012cd09a9b256d870751284dd6a29882b0be105
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Int.Order.Basic
import Mathlib.Data.Int.Units
import Mathlib.Algebra.GroupPower.Order

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

namespace Int

theorem isUnit_iff_abs_eq: ∀ {x : ℤ}, IsUnit x ↔ abs x = 1isUnit_iff_abs_eq {x: ℤx : ℤ: Typeℤ} : IsUnit: {M : Type ?u.4} → [inst : Monoid M] → M → PropIsUnit x: ℤx ↔ abs: {α : Type ?u.15} → [self : Abs α] → α → αabs x: ℤx = 1: ?m.1211 := byGoals accomplished! 🐙
x: ℤIsUnit x ↔ abs x = 1rw [x: ℤIsUnit x ↔ abs x = 1isUnit_iff_natAbs_eq: ∀ {n : ℤ}, IsUnit n ↔ natAbs n = 1isUnit_iff_natAbs_eq,x: ℤnatAbs x = 1 ↔ abs x = 1 x: ℤIsUnit x ↔ abs x = 1abs_eq_natAbs: ∀ (a : ℤ), abs a = ↑(natAbs a)abs_eq_natAbs,x: ℤnatAbs x = 1 ↔ ↑(natAbs x) = 1 x: ℤIsUnit x ↔ abs x = 1← Int.ofNat_one: ↑1 = 1Int.ofNat_one,x: ℤnatAbs x = 1 ↔ ↑(natAbs x) = ↑1 x: ℤIsUnit x ↔ abs x = 1coe_nat_inj': ∀ {m n : ℕ}, ↑m = ↑n ↔ m = ncoe_nat_inj'x: ℤnatAbs x = 1 ↔ natAbs x = 1]Goals accomplished! 🐙
#align int.is_unit_iff_abs_eq Int.isUnit_iff_abs_eq: ∀ {x : ℤ}, IsUnit x ↔ abs x = 1Int.isUnit_iff_abs_eq

theorem isUnit_sq: ∀ {a : ℤ}, IsUnit a → a ^ 2 = 1isUnit_sq {a: ℤa : ℤ: Typeℤ} (ha: IsUnit aha : IsUnit: {M : Type ?u.198} → [inst : Monoid M] → M → PropIsUnit a: ℤa) : a: ℤa ^ 2: ?m.2322 = 1: ?m.2461 := byGoals accomplished! 🐙 a: ℤha: IsUnit aa ^ 2 = 1rw [a: ℤha: IsUnit aa ^ 2 = 1sq: ∀ {M : Type ?u.441} [inst : Monoid M] (a : M), a ^ 2 = a * asq,a: ℤha: IsUnit aa * a = 1 a: ℤha: IsUnit aa ^ 2 = 1isUnit_mul_self: ∀ {a : ℤ}, IsUnit a → a * a = 1isUnit_mul_self ha: IsUnit ahaa: ℤha: IsUnit a1 = 1]Goals accomplished! 🐙
#align int.is_unit_sq Int.isUnit_sq: ∀ {a : ℤ}, IsUnit a → a ^ 2 = 1Int.isUnit_sq

@[simp]
theorem units_sq: ∀ (u : ℤˣ), u ^ 2 = 1units_sq (u: ℤˣu : ℤ: Typeℤˣ) : u: ℤˣu ^ 2: ?m.5332 = 1: ?m.5471 := byGoals accomplished! 🐙
u: ℤˣu ^ 2 = 1rw [u: ℤˣu ^ 2 = 1Units.ext_iff: ∀ {α : Type ?u.1230} [inst : Monoid α] {a b : αˣ}, a = b ↔ ↑a = ↑bUnits.ext_iff,u: ℤˣ↑(u ^ 2) = ↑1 u: ℤˣu ^ 2 = 1Units.val_pow_eq_pow_val: ∀ {M : Type ?u.1276} [inst : Monoid M] (u : Mˣ) (n : ℕ), ↑(u ^ n) = ↑u ^ nUnits.val_pow_eq_pow_val,u: ℤˣ↑u ^ 2 = ↑1 u: ℤˣu ^ 2 = 1Units.val_one: ∀ {α : Type ?u.1331} [inst : Monoid α], ↑1 = 1Units.val_one,u: ℤˣ↑u ^ 2 = 1 u: ℤˣu ^ 2 = 1isUnit_sq: ∀ {a : ℤ}, IsUnit a → a ^ 2 = 1isUnit_sq u: ℤˣu.isUnit: ∀ {M : Type ?u.1387} [inst : Monoid M] (u : Mˣ), IsUnit ↑uisUnitu: ℤˣ1 = 1]Goals accomplished! 🐙
#align int.units_sq Int.units_sq: ∀ (u : ℤˣ), u ^ 2 = 1Int.units_sq

alias units_sq: ∀ (u : ℤˣ), u ^ 2 = 1units_sq ← units_pow_two: ∀ (u : ℤˣ), u ^ 2 = 1units_pow_two
#align int.units_pow_two Int.units_pow_two: ∀ (u : ℤˣ), u ^ 2 = 1Int.units_pow_two

@[simp]
theorem units_mul_self: ∀ (u : ℤˣ), u * u = 1units_mul_self (u: ℤˣu : ℤ: Typeℤˣ) : u: ℤˣu * u: ℤˣu = 1: ?m.14411 := byGoals accomplished! 🐙 u: ℤˣu * u = 1rw [u: ℤˣu * u = 1← sq: ∀ {M : Type ?u.2331} [inst : Monoid M] (a : M), a ^ 2 = a * asq,u: ℤˣu ^ 2 = 1 u: ℤˣu * u = 1units_sq: ∀ (u : ℤˣ), u ^ 2 = 1units_squ: ℤˣ1 = 1]Goals accomplished! 🐙
#align int.units_mul_self Int.units_mul_self: ∀ (u : ℤˣ), u * u = 1Int.units_mul_self

@[simp]
theorem units_inv_eq_self: ∀ (u : ℤˣ), u⁻¹ = uunits_inv_eq_self (u: ℤˣu : ℤ: Typeℤˣ) : u: ℤˣu⁻¹ = u: ℤˣu := byGoals accomplished! 🐙 u: ℤˣu⁻¹ = urw [u: ℤˣu⁻¹ = uinv_eq_iff_mul_eq_one: ∀ {G : Type ?u.2636} [inst : Group G] {a b : G}, a⁻¹ = b ↔ a * b = 1inv_eq_iff_mul_eq_one,u: ℤˣu * u = 1 u: ℤˣu⁻¹ = uunits_mul_self: ∀ (u : ℤˣ), u * u = 1units_mul_selfu: ℤˣ1 = 1]Goals accomplished! 🐙
#align int.units_inv_eq_self Int.units_inv_eq_self: ∀ (u : ℤˣ), u⁻¹ = uInt.units_inv_eq_self

-- `Units.val_mul` is a "wrong turn" for the simplifier, this undoes it and simplifies further
@[simp]
theorem units_coe_mul_self: ∀ (u : ℤˣ), ↑u * ↑u = 1units_coe_mul_self (u: ℤˣu : ℤ: Typeℤˣ) : (u: ℤˣu * u: ℤˣu : ℤ: Typeℤ) = 1: ?m.58221 := byGoals accomplished! 🐙
u: ℤˣ↑u * ↑u = 1rw [u: ℤˣ↑u * ↑u = 1← Units.val_mul: ∀ {α : Type ?u.5850} [inst : Monoid α] (a b : αˣ), ↑(a * b) = ↑a * ↑bUnits.val_mul,u: ℤˣ↑(u * u) = 1 u: ℤˣ↑u * ↑u = 1units_mul_self: ∀ (u : ℤˣ), u * u = 1units_mul_self,u: ℤˣ↑1 = 1 u: ℤˣ↑u * ↑u = 1Units.val_one: ∀ {α : Type ?u.5909} [inst : Monoid α], ↑1 = 1Units.val_oneu: ℤˣ1 = 1]Goals accomplished! 🐙
#align int.units_coe_mul_self Int.units_coe_mul_self: ∀ (u : ℤˣ), ↑u * ↑u = 1Int.units_coe_mul_self

@[simp]
theorem neg_one_pow_ne_zero: ∀ {n : ℕ}, (-1) ^ n ≠ 0neg_one_pow_ne_zero {n: ℕn : ℕ: Typeℕ} : (-1: ?m.60401 : ℤ: Typeℤ) ^ n: ℕn ≠ 0: ?m.62150 :=
pow_ne_zero: ∀ {M : Type ?u.6224} [inst : MonoidWithZero M] [inst_1 : NoZeroDivisors M] {a : M} (n : ℕ), a ≠ 0 → a ^ n ≠ 0pow_ne_zero _: ℕ_ (abs_pos: ∀ {α : Type ?u.6311} [inst : AddGroup α] [inst_1 : LinearOrder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α}, 0 < abs a ↔ a ≠ 0abs_pos.mp: ∀ {a b : Prop}, (a ↔ b) → a → bmp (byGoals accomplished! 🐙 n: ℕ0 < abs (-1)simpGoals accomplished! 🐙))
#align int.neg_one_pow_ne_zero Int.neg_one_pow_ne_zero: ∀ {n : ℕ}, (-1) ^ n ≠ 0Int.neg_one_pow_ne_zero

theorem sq_eq_one_of_sq_lt_four: ∀ {x : ℤ}, x ^ 2 < 4 → x ≠ 0 → x ^ 2 = 1sq_eq_one_of_sq_lt_four {x: ℤx : ℤ: Typeℤ} (h1: x ^ 2 < 4h1 : x: ℤx ^ 2: ?m.66642 < 4: ?m.66784) (h2: x ≠ 0h2 : x: ℤx ≠ 0: ?m.68300) : x: ℤx ^ 2: ?m.68432 = 1: ?m.68571 :=
sq_eq_one_iff: ∀ {R : Type ?u.7036} [inst : Ring R] {a : R} [inst_1 : NoZeroDivisors R], a ^ 2 = 1 ↔ a = 1 ∨ a = -1sq_eq_one_iff.mpr: ∀ {a b : Prop}, (a ↔ b) → b → ampr
((abs_eq: ∀ {α : Type ?u.7090} [inst : LinearOrderedAddCommGroup α] {a b : α}, 0 ≤ b → (abs a = b ↔ a = b ∨ a = -b)abs_eq (zero_le_one': ∀ (α : Type ?u.7095) [inst : Zero α] [inst_1 : One α] [inst_2 : LE α] [inst_3 : ZeroLEOneClass α], 0 ≤ 1zero_le_one' ℤ: Typeℤ)).mp: ∀ {a b : Prop}, (a ↔ b) → a → bmp
(le_antisymm: ∀ {α : Type ?u.7331} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≤ a → a = ble_antisymm (lt_add_one_iff: ∀ {a b : ℤ}, a < b + 1 ↔ a ≤ blt_add_one_iff.mp: ∀ {a b : Prop}, (a ↔ b) → a → bmp (abs_lt_of_sq_lt_sq: ∀ {R : Type ?u.7406} [inst : LinearOrderedRing R] {x y : R}, x ^ 2 < y ^ 2 → 0 ≤ y → abs x < yabs_lt_of_sq_lt_sq h1: x ^ 2 < 4h1 zero_le_two: ∀ {α : Type ?u.7506} [inst : AddMonoidWithOne α] [inst_1 : Preorder α] [inst_2 : ZeroLEOneClass α]
[inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], 0 ≤ 2zero_le_two))
(sub_one_lt_iff: ∀ {a b : ℤ}, a - 1 < b ↔ a ≤ bsub_one_lt_iff.mp: ∀ {a b : Prop}, (a ↔ b) → a → bmp (abs_pos: ∀ {α : Type ?u.7839} [inst : AddGroup α] [inst_1 : LinearOrder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α}, 0 < abs a ↔ a ≠ 0abs_pos.mpr: ∀ {a b : Prop}, (a ↔ b) → b → ampr h2: x ≠ 0h2))))
#align int.sq_eq_one_of_sq_lt_four Int.sq_eq_one_of_sq_lt_four: ∀ {x : ℤ}, x ^ 2 < 4 → x ≠ 0 → x ^ 2 = 1Int.sq_eq_one_of_sq_lt_four

theorem sq_eq_one_of_sq_le_three: ∀ {x : ℤ}, x ^ 2 ≤ 3 → x ≠ 0 → x ^ 2 = 1sq_eq_one_of_sq_le_three {x: ℤx : ℤ: Typeℤ} (h1: x ^ 2 ≤ 3h1 : x: ℤx ^ 2: ?m.80892 ≤ 3: ?m.81033) (h2: x ≠ 0h2 : x: ℤx ≠ 0: ?m.82550) : x: ℤx ^ 2: ?m.82682 = 1: ?m.82821 :=
sq_eq_one_of_sq_lt_four: ∀ {x : ℤ}, x ^ 2 < 4 → x ≠ 0 → x ^ 2 = 1sq_eq_one_of_sq_lt_four (lt_of_le_of_lt: ∀ {α : Type ?u.8471} [inst : Preorder α] {a b c : α}, a ≤ b → b < c → a < clt_of_le_of_lt h1: x ^ 2 ≤ 3h1 (lt_add_one: ∀ {α : Type ?u.8552} [inst : One α] [inst_1 : AddZeroClass α] [inst_2 : PartialOrder α] [inst_3 : ZeroLEOneClass α]
[inst_4 : NeZero 1] [inst_5 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] (a : α), a < a + 1lt_add_one (3: ?m.85623 : ℤ: Typeℤ))) h2: x ≠ 0h2
#align int.sq_eq_one_of_sq_le_three Int.sq_eq_one_of_sq_le_three: ∀ {x : ℤ}, x ^ 2 ≤ 3 → x ≠ 0 → x ^ 2 = 1Int.sq_eq_one_of_sq_le_three

theorem units_pow_eq_pow_mod_two: ∀ (u : ℤˣ) (n : ℕ), u ^ n = u ^ (n % 2)units_pow_eq_pow_mod_two (u: ℤˣu : ℤ: Typeℤˣ) (n: ℕn : ℕ: Typeℕ) : u: ℤˣu ^ n: ℕn = u: ℤˣu ^ (n: ℕn % 2: ?m.89122) := byGoals accomplished! 🐙
u: ℤˣn: ℕu ^ n = u ^ (n % 2)conv =>u: ℤˣn: ℕu ^ (n % 2)
u: ℤˣn: ℕu ^ n = u ^ (n % 2)lhsu: ℤˣn: ℕu ^ n
u: ℤˣn: ℕu ^ n = u ^ (n % 2)rw [u: ℤˣn: ℕu ^ n← Nat.mod_add_div: ∀ (m k : ℕ), m % k + k * (m / k) = mNat.mod_add_div n: ℕn 2: ?m.128022u: ℤˣn: ℕu ^ (n % 2 + 2 * (n / 2))]u: ℤˣn: ℕu ^ (n % 2 + 2 * (n / 2));u: ℤˣn: ℕu ^ (n % 2 + 2 * (n / 2))
u: ℤˣn: ℕu ^ n = u ^ (n % 2)rw [u: ℤˣn: ℕu ^ (n % 2 + 2 * (n / 2))pow_add: ∀ {M : Type ?u.12807} [inst : Monoid M] (a : M) (m n : ℕ), a ^ (m + n) = a ^ m * a ^ npow_add,u: ℤˣn: ℕu ^ (n % 2) * u ^ (2 * (n / 2)) u: ℤˣn: ℕu ^ (n % 2 + 2 * (n / 2))pow_mul: ∀ {M : Type ?u.13038} [inst : Monoid M] (a : M) (m n : ℕ), a ^ (m * n) = (a ^ m) ^ npow_mul,u: ℤˣn: ℕu ^ (n % 2) * (u ^ 2) ^ (n / 2) u: ℤˣn: ℕu ^ (n % 2 + 2 * (n / 2))units_sq: ∀ (u : ℤˣ), u ^ 2 = 1units_sq,u: ℤˣn: ℕu ^ (n % 2) * 1 ^ (n / 2) u: ℤˣn: ℕu ^ (n % 2 + 2 * (n / 2))one_pow: ∀ {M : Type ?u.13124} [inst : Monoid M] (n : ℕ), 1 ^ n = 1one_pow,u: ℤˣn: ℕu ^ (n % 2) * 1 u: ℤˣn: ℕu ^ (n % 2 + 2 * (n / 2))mul_one: ∀ {M : Type ?u.13243} [inst : MulOneClass M] (a : M), a * 1 = amul_oneu: ℤˣn: ℕu ^ (n % 2)]u: ℤˣn: ℕu ^ (n % 2)
#align int.units_pow_eq_pow_mod_two Int.units_pow_eq_pow_mod_two: ∀ (u : ℤˣ) (n : ℕ), u ^ n = u ^ (n % 2)Int.units_pow_eq_pow_mod_two

end Int
```