Mathlib.Data.Int.Order.Units

Int.isUnit_iff_abs_eq theorem

{x : ℤ} : IsUnit x ↔ abs x = 1

Full source

theorem isUnit_iff_abs_eq {x : ℤ} : IsUnitIsUnit x ↔ abs x = 1 := by
  rw [isUnit_iff_natAbs_eq, abs_eq_natAbs, ← Int.ofNat_one, natCast_inj]

Characterization of Integer Units via Absolute Value: $x$ is a unit iff $|x| = 1$

Informal description

An integer $x$ is a unit in the multiplicative monoid of integers if and only if its absolute value equals 1, i.e., $|x| = 1$.

Int.isUnit_sq theorem

{a : ℤ} (ha : IsUnit a) : a ^ 2 = 1

Full source

theorem isUnit_sq {a : ℤ} (ha : IsUnit a) : a ^ 2 = 1 := by rw [sq, isUnit_mul_self ha]

Square of Integer Unit Equals One

Informal description

For any integer $a$ that is a unit in the multiplicative monoid of integers, the square of $a$ equals $1$, i.e., $a^2 = 1$.

Int.units_sq theorem

(u : ℤˣ) : u ^ 2 = 1

Full source

@[simp]
theorem units_sq (u : ℤℤˣ) : u ^ 2 = 1 := by
  rw [Units.ext_iff, Units.val_pow_eq_pow_val, Units.val_one, isUnit_sq u.isUnit]

Square of Integer Unit Equals One: $u^2 = 1$ for $u \in \mathbb{Z}^\times$

Informal description

For any unit $u$ in the multiplicative group of integers $\mathbb{Z}^\times$, the square of $u$ equals the multiplicative identity, i.e., $u^2 = 1$.

Int.units_mul_self theorem

(u : ℤˣ) : u * u = 1

Full source

@[simp]
theorem units_mul_self (u : ℤℤˣ) : u * u = 1 := by rw [← sq, units_sq]

Square of Integer Unit Equals One: $u \cdot u = 1$ for $u \in \mathbb{Z}^\times$

Informal description

For any unit $u$ in the multiplicative group of integers $\mathbb{Z}^\times$, the product of $u$ with itself equals the multiplicative identity, i.e., $u \cdot u = 1$.

Int.units_inv_eq_self theorem

(u : ℤˣ) : u⁻¹ = u

Full source

@[simp]
theorem units_inv_eq_self (u : ℤℤˣ) : u⁻¹ = u := by rw [inv_eq_iff_mul_eq_one, units_mul_self]

Inverse of Integer Unit Equals Itself: $u^{-1} = u$ for $u \in \mathbb{Z}^\times$

Informal description

For any unit $u$ in the multiplicative group of integers $\mathbb{Z}^\times$, the inverse of $u$ is equal to $u$ itself, i.e., $u^{-1} = u$.

Int.units_div_eq_mul theorem

(u₁ u₂ : ℤˣ) : u₁ / u₂ = u₁ * u₂

Full source

theorem units_div_eq_mul (u₁ u₂ : ℤℤˣ) : u₁ / u₂ = u₁ * u₂ := by
  rw [div_eq_mul_inv, units_inv_eq_self]

Division of Integer Units Equals Multiplication: $u_1 / u_2 = u_1 \cdot u_2$ for $u_1, u_2 \in \mathbb{Z}^\times$

Informal description

For any units $u_1, u_2$ in the multiplicative group of integers $\mathbb{Z}^\times$, the division operation satisfies $u_1 / u_2 = u_1 \cdot u_2$.

Int.units_coe_mul_self theorem

(u : ℤˣ) : (u * u : ℤ) = 1

Full source

@[simp]
theorem units_coe_mul_self (u : ℤℤˣ) : (u * u : ℤ) = 1 := by
  rw [← Units.val_mul, units_mul_self, Units.val_one]

Square of Integer Unit as Integer Equals One: $(u \cdot u) = 1$ for $u \in \mathbb{Z}^\times$

Informal description

For any unit $u$ in the multiplicative group of integers $\mathbb{Z}^\times$, the product of $u$ with itself, when viewed as an integer, equals $1$, i.e., $(u \cdot u) = 1$ where the multiplication is performed in $\mathbb{Z}$.

Int.neg_one_pow_ne_zero theorem

{n : ℕ} : (-1 : ℤ) ^ n ≠ 0

Full source

theorem neg_one_pow_ne_zero {n : ℕ} : (-1 : ℤ) ^ n ≠ 0 := by simp

Non-vanishing of $(-1)^n$ for $n \in \mathbb{N}$

Informal description

For any natural number $n$, the integer $(-1)^n$ is nonzero.

Int.sq_eq_one_of_sq_lt_four theorem

{x : ℤ} (h1 : x ^ 2 < 4) (h2 : x ≠ 0) : x ^ 2 = 1

Full source

theorem sq_eq_one_of_sq_lt_four {x : ℤ} (h1 : x ^ 2 < 4) (h2 : x ≠ 0) : x ^ 2 = 1 :=
  sq_eq_one_iff.mpr
    ((abs_eq (zero_le_one' ℤ)).mp
      (le_antisymm (lt_add_one_iff.mp (abs_lt_of_sq_lt_sq h1 zero_le_two))
        (sub_one_lt_iff.mp (abs_pos.mpr h2))))

Integer squares less than four are one: $x^2 < 4 \land x \neq 0 \implies x^2 = 1$

Informal description

For any integer $x$ such that $x^2 < 4$ and $x \neq 0$, we have $x^2 = 1$.

Int.sq_eq_one_of_sq_le_three theorem

{x : ℤ} (h1 : x ^ 2 ≤ 3) (h2 : x ≠ 0) : x ^ 2 = 1

Full source

theorem sq_eq_one_of_sq_le_three {x : ℤ} (h1 : x ^ 2 ≤ 3) (h2 : x ≠ 0) : x ^ 2 = 1 :=
  sq_eq_one_of_sq_lt_four (lt_of_le_of_lt h1 (lt_add_one (3 : ℤ))) h2

Integer squares at most three are one: $x^2 \leq 3 \land x \neq 0 \implies x^2 = 1$

Informal description

For any integer $x$ such that $x^2 \leq 3$ and $x \neq 0$, we have $x^2 = 1$.

Int.units_pow_eq_pow_mod_two theorem

(u : ℤˣ) (n : ℕ) : u ^ n = u ^ (n % 2)

Full source

theorem units_pow_eq_pow_mod_two (u : ℤℤˣ) (n : ℕ) : u ^ n = u ^ (n % 2) := by
  conv =>
    lhs
    rw [← Nat.mod_add_div n 2]
    rw [pow_add, pow_mul, units_sq, one_pow, mul_one]

Powers of Integer Units Modulo Two: $u^n = u^{n \mod 2}$ for $u \in \mathbb{Z}^\times$

Informal description

For any unit $u$ in the multiplicative group of integers $\mathbb{Z}^\times$ and any natural number $n$, the $n$-th power of $u$ equals the $(n \mod 2)$-th power of $u$, i.e., $u^n = u^{n \mod 2}$.