G : Type u
A : Type v
x y : G
a b : A
n m✝ : ℕ
inst✝² : Group G
inst✝¹ : AddGroup A
inst✝ : Fintype G
h : x ^ gcd n (Fintype.card G) = 1
m : ℕ
hm : n = gcd n (Fintype.card G) * m
⊢ x ^ n = 1
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝² : Group G
inst✝¹ : AddGroup A
inst✝ : Fintype G
h : x ^ gcd n (Fintype.card G) = 1
⊢ x ^ n = 1
let ⟨m, hm⟩ := gcd_dvd_left n (Fintype.card G)
no goals
G : Type u
A : Type v
x y : G
a b : A
n m✝ : ℕ
inst✝² : Group G
inst✝¹ : AddGroup A
inst✝ : Fintype G
h : x ^ gcd n (Fintype.card G) = 1
m : ℕ
hm : n = gcd n (Fintype.card G) * m
⊢ x ^ n = 1
rw [hm, pow_mul, h, one_pow]