pow_index_mem — Mathlib

English

If gcd(|G|, n) = 1 for a finite group G, the map x ↦ x^n is a bijection on G.

Русский

Если gcd(|G|, n) = 1, отображение x ↦ x^n на группе G является биекцией.

LaTeX

$$If $\gcd(|G|, n) = 1$, then the map $x \mapsto x^n$ is bijective on G.$$

Lean4

@[to_additive]
theorem pow_index_mem {G : Type*} [Group G] (H : Subgroup G) [Normal H] (g : G) : g ^ index H ∈ H := by
  rw [← eq_one_iff, QuotientGroup.mk_pow H, index, pow_card_eq_one']

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