English
There exists for each n with gcd(p, n) = 1 a p-group preserving equivalence hG.powEquiv hn : G ≃ G.
Русский
Для каждого n с gcd(p, n) = 1 существует биекция hG.powEquiv hn : G ≃ G, сохраняющая p-групповость.
LaTeX
$$$\IsPGroup(p,G) \rightarrow \forall {n}, \; p.Coprime n \rightarrow G \cong G$$$
Lean4
/-- If `gcd(p,n) = 1`, then the `n`th power map is a bijection. -/
noncomputable def powEquiv {n : ℕ} (hn : p.Coprime n) : G ≃ G :=
let h : ∀ g : G, (Nat.card (Subgroup.zpowers g)).Coprime n := fun g =>
(Nat.card_zpowers g).symm ▸ hG.orderOf_coprime hn g
{ toFun := (· ^ n)
invFun := fun g => (powCoprime (h g)).symm ⟨g, Subgroup.mem_zpowers g⟩
left_inv := fun g =>
Subtype.ext_iff.1 <|
(powCoprime (h (g ^ n))).left_inv
⟨g, _, Subtype.ext_iff.1 <| (powCoprime (h g)).left_inv ⟨g, Subgroup.mem_zpowers g⟩⟩
right_inv := fun g => Subtype.ext_iff.1 <| (powCoprime (h g)).right_inv ⟨g, Subgroup.mem_zpowers g⟩ }
