zpow_mod_natCard — Mathlib

English

If gcd(|G|, n) = 1, powCoprime h is an equivalence, with inverse mapping g ↦ g^{|G| gcd B n}.

Русский

Если gcd(|G|, n) = 1, отображение powCoprime является эквиваленцией с обратным отображением g ↦ g^{|G| gcd(n)}.

LaTeX

$$powCoprime h : G ≃ G$$

Lean4

@[to_additive (attr := simp) mod_natCard_zsmul]
theorem zpow_mod_natCard {G} [Group G] (a : G) (n : ℤ) : a ^ (n % Nat.card G : ℤ) = a ^ n := by
  rw [eq_comm, ← zpow_mod_orderOf, ← Int.emod_emod_of_dvd n <| Int.natCast_dvd_natCast.2 <| orderOf_dvd_natCard _,
    zpow_mod_orderOf]

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