case intro
M : Type ?u.3545896
N : Type ?u.3545899
G : Type ?u.3545902
R : Type u_1
S : Type ?u.3545908
F : Type ?u.3545911
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k l : ℕ
inst✝¹ : CommRing R
ζ✝¹ : Rˣ
h✝ : IsPrimitiveRoot ζ✝¹ k
inst✝ : IsDomain R
ζ✝ : R
n : ℕ+
h : IsPrimitiveRoot ζ✝ ↑n
ζ : Rˣ
hζ : ↑ζ = ζ✝
⊢ Fintype.card { x // x ∈ rootsOfUnity n R } = ↑n
M : Type ?u.3545896
N : Type ?u.3545899
G : Type ?u.3545902
R : Type u_1
S : Type ?u.3545908
F : Type ?u.3545911
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k
inst✝ : IsDomain R
ζ : R
n : ℕ+
h : IsPrimitiveRoot ζ ↑n
⊢ Fintype.card { x // x ∈ rootsOfUnity n R } = ↑n
obtain ⟨ζ, hζ⟩ := h.isUnit n.pos
case intro
M : Type ?u.3545896
N : Type ?u.3545899
G : Type ?u.3545902
R : Type u_1
S : Type ?u.3545908
F : Type ?u.3545911
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k l : ℕ
inst✝¹ : CommRing R
ζ✝¹ : Rˣ
h✝ : IsPrimitiveRoot ζ✝¹ k
inst✝ : IsDomain R
ζ✝ : R
n : ℕ+
ζ : Rˣ
h : IsPrimitiveRoot ζ ↑n
hζ : ↑ζ = ζ✝
⊢ Fintype.card { x // x ∈ rootsOfUnity n R } = ↑n
case intro
M : Type ?u.3545896
N : Type ?u.3545899
G : Type ?u.3545902
R : Type u_1
S : Type ?u.3545908
F : Type ?u.3545911
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k l : ℕ
inst✝¹ : CommRing R
ζ✝¹ : Rˣ
h✝ : IsPrimitiveRoot ζ✝¹ k
inst✝ : IsDomain R
ζ✝ : R
n : ℕ+
h : IsPrimitiveRoot ζ✝ ↑n
ζ : Rˣ
hζ : ↑ζ = ζ✝
⊢ Fintype.card { x // x ∈ rootsOfUnity n R } = ↑n
rw [← hζ, IsPrimitiveRoot.coe_units_iff] at h
no goals
case intro
M : Type ?u.3545896
N : Type ?u.3545899
G : Type ?u.3545902
R : Type u_1
S : Type ?u.3545908
F : Type ?u.3545911
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k l : ℕ
inst✝¹ : CommRing R
ζ✝¹ : Rˣ
h✝ : IsPrimitiveRoot ζ✝¹ k
inst✝ : IsDomain R
ζ✝ : R
n : ℕ+
ζ : Rˣ
h : IsPrimitiveRoot ζ ↑n
hζ : ↑ζ = ζ✝
⊢ Fintype.card { x // x ∈ rootsOfUnity n R } = ↑n
exact h.card_rootsOfUnity'