p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
n : ℕ
hn : Nat.coprime p n
g : G
⊢ ↑(powEquiv hG hn).symm g = g ^ Nat.gcdB (Nat.card { x // x ∈ Subgroup.zpowers g }) n
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
n : ℕ
hn : Nat.coprime p n
g : G
⊢ ↑(powEquiv hG hn).symm g = g ^ Nat.gcdB (orderOf g) n
rw [order_eq_card_zpowers']
no goals
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
n : ℕ
hn : Nat.coprime p n
g : G
⊢ ↑(powEquiv hG hn).symm g = g ^ Nat.gcdB (Nat.card { x // x ∈ Subgroup.zpowers g }) n
rfl