zpow_mod_card — Mathlib

English

If gcd(|G|, n) = 1, then powCoprime h g^{-1} = (powCoprime h g)^{-1}.

Русский

Если gcd(|G|, n) = 1, то powCoprime h g^{-1} = (powCoprime h g)^{-1}.

LaTeX

$$powCoprime h g^{-1} = (powCoprime h g)^{-1}$$

Lean4

@[to_additive (attr := simp) mod_card_zsmul]
theorem zpow_mod_card (a : G) (n : ℤ) : a ^ (n % Fintype.card G : ℤ) = a ^ n := by
  rw [eq_comm, ← zpow_mod_orderOf, ← Int.emod_emod_of_dvd n (Int.natCast_dvd_natCast.2 orderOf_dvd_card),
    zpow_mod_orderOf]

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