pow_mod_natCard — Mathlib

English

If gcd(|G|, n) = 1, then the left n-th power map is bijective on G, i.e., the left action by n is invertible.

Русский

При взаимно простых |G| и n отображение возведения в степень n слева на G — биекция.

LaTeX

$$pow_left_bijective {G} [Group G] (hn : (Nat.card G).Coprime n) : Bijective (\u00b7 ^ n : G \to G)$$

Lean4

@[to_additive (attr := simp) mod_natCard_nsmul]
theorem pow_mod_natCard {G} [Group G] (a : G) (n : ℕ) : a ^ (n % Nat.card G) = a ^ n := by
  rw [eq_comm, ← pow_mod_orderOf, ← Nat.mod_mod_of_dvd n <| orderOf_dvd_natCard _, pow_mod_orderOf]

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