case a
M : Type ?u.3298392
N : Type ?u.3298395
G : Type ?u.3298398
R : Type u_1
S : Type ?u.3298404
F : Type ?u.3298407
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
k : ℕ+
ζ : Rˣ
h : IsPrimitiveRoot ζ ↑k
⊢ ↑(Subgroup.zpowers ζ) = ↑(rootsOfUnity k R)
M : Type ?u.3298392
N : Type ?u.3298395
G : Type ?u.3298398
R : Type u_1
S : Type ?u.3298404
F : Type ?u.3298407
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
k : ℕ+
ζ : Rˣ
h : IsPrimitiveRoot ζ ↑k
⊢ Subgroup.zpowers ζ = rootsOfUnity k R
apply SetLike.coe_injective
case a
M : Type ?u.3298392
N : Type ?u.3298395
G : Type ?u.3298398
R : Type u_1
S : Type ?u.3298404
F✝ : Type ?u.3298407
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
k : ℕ+
ζ : Rˣ
h : IsPrimitiveRoot ζ ↑k
F : Fintype { x // x ∈ Subgroup.zpowers ζ }
⊢ ↑(Subgroup.zpowers ζ) = ↑(rootsOfUnity k R)
case a
M : Type ?u.3298392
N : Type ?u.3298395
G : Type ?u.3298398
R : Type u_1
S : Type ?u.3298404
F : Type ?u.3298407
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
k : ℕ+
ζ : Rˣ
h : IsPrimitiveRoot ζ ↑k
⊢ ↑(Subgroup.zpowers ζ) = ↑(rootsOfUnity k R)
haveI F : Fintype (Subgroup.zpowers ζ) := Fintype.ofEquiv _ h.zmodEquivZpowers.toEquiv
case a
M : Type ?u.3298392
N : Type ?u.3298395
G : Type ?u.3298398
R : Type u_1
S : Type ?u.3298404
F✝ : Type ?u.3298407
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
k : ℕ+
ζ : Rˣ
h : IsPrimitiveRoot ζ ↑k
F : Fintype { x // x ∈ Subgroup.zpowers ζ }
⊢ Fintype.card ↑↑(rootsOfUnity k R) ≤ Fintype.card ↑↑(Subgroup.zpowers ζ)
case a
M : Type ?u.3298392
N : Type ?u.3298395
G : Type ?u.3298398
R : Type u_1
S : Type ?u.3298404
F✝ : Type ?u.3298407
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
k : ℕ+
ζ : Rˣ
h : IsPrimitiveRoot ζ ↑k
F : Fintype { x // x ∈ Subgroup.zpowers ζ }
⊢ ↑(Subgroup.zpowers ζ) = ↑(rootsOfUnity k R)
refine'
  @Set.eq_of_subset_of_card_le Rˣ (Subgroup.zpowers ζ) (rootsOfUnity k R) F
    (rootsOfUnity.fintype R k)
    (Subgroup.zpowers_le_of_mem <| show ζ ∈ rootsOfUnity k R from h.pow_eq_one) _
no goals
case a
M : Type ?u.3298392
N : Type ?u.3298395
G : Type ?u.3298398
R : Type u_1
S : Type ?u.3298404
F✝ : Type ?u.3298407
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
k : ℕ+
ζ : Rˣ
h : IsPrimitiveRoot ζ ↑k
F : Fintype { x // x ∈ Subgroup.zpowers ζ }
⊢ Fintype.card ↑↑(rootsOfUnity k R) ≤ Fintype.card ↑↑(Subgroup.zpowers ζ)
calc
  Fintype.card (rootsOfUnity k R) ≤ k := card_rootsOfUnity R k
  _ = Fintype.card (ZMod k) := (ZMod.card k).symm
  _ = Fintype.card (Subgroup.zpowers ζ) := Fintype.card_congr h.zmodEquivZpowers.toEquiv