units_pow_eq_pow_mod_two — Mathlib

English

Let u be a unit in the integers and n a natural number. Then the power u^n depends only on the parity of n; in fact u^n = u^(n mod 2).

Русский

Пусть u — единица в целых, а n ∈ ℕ. Тогда степень u^n зависит только от парности n; то есть u^n = u^(n mod 2).

LaTeX

$$$\forall u \in \mathbb{Z}^{\times}, \; \forall n \in \mathbb{N},\; u^n = u^{\,n \\bmod 2}$$$

Lean4

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]

Похожие утверждения