case a
G : Type u
A : Type v
x✝ y : G
a b : A
n m : ℕ
inst✝³ : Group G
inst✝² : AddGroup A
inst✝¹ : Fintype G
inst✝ : DecidableEq G
x : G
⊢ x ∈ Finset.image (fun i => x✝ ^ i) (Finset.range (orderOf x✝)) ↔ x ∈ Set.toFinset ↑(zpowers x✝)
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝³ : Group G
inst✝² : AddGroup A
inst✝¹ : Fintype G
inst✝ : DecidableEq G
⊢ Finset.image (fun i => x ^ i) (Finset.range (orderOf x)) = Set.toFinset ↑(zpowers x)
ext x
no goals
case a
G : Type u
A : Type v
x✝ y : G
a b : A
n m : ℕ
inst✝³ : Group G
inst✝² : AddGroup A
inst✝¹ : Fintype G
inst✝ : DecidableEq G
x : G
⊢ x ∈ Finset.image (fun i => x✝ ^ i) (Finset.range (orderOf x✝)) ↔ x ∈ Set.toFinset ↑(zpowers x✝)
rw [Set.mem_toFinset, SetLike.mem_coe, mem_zpowers_iff_mem_range_orderOf]