zpow_mod_orderOf — Mathlib

English

For any x in a group and any integer z, x^(z mod orderOf x) = x^z.

Русский

Для любого x в группе и любого целого z выполняется x^(z mod orderOf x) = x^z.

LaTeX

$$x^(z mod (orderOf x)) = x^z$$

Lean4

@[to_additive mod_addOrderOf_zsmul]
theorem zpow_mod_orderOf (x : G) (z : ℤ) : x ^ (z % (orderOf x : ℤ)) = x ^ z :=
  calc
    x ^ (z % (orderOf x : ℤ)) = x ^ (z % orderOf x + orderOf x * (z / orderOf x) : ℤ) := by
      simp [zpow_add, zpow_mul, pow_orderOf_eq_one]
    _ = x ^ z := by rw [Int.emod_add_mul_ediv]

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