case pos
M : Type ?u.3642802
N : Type ?u.3642805
G : Type ?u.3642808
R : Type u_1
S : Type ?u.3642814
F : Type ?u.3642817
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
hn : n = 0
⊢ nthRootsFinset n R = Finset.biUnion (Nat.divisors n) fun i => primitiveRoots i R

case neg
M : Type ?u.3642802
N : Type ?u.3642805
G : Type ?u.3642808
R : Type u_1
S : Type ?u.3642814
F : Type ?u.3642817
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
hn : ¬n = 0
⊢ nthRootsFinset n R = Finset.biUnion (Nat.divisors n) fun i => primitiveRoots i R
M : Type ?u.3642802
N : Type ?u.3642805
G : Type ?u.3642808
R : Type u_1
S : Type ?u.3642814
F : Type ?u.3642817
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
⊢ nthRootsFinset n R = Finset.biUnion (Nat.divisors n) fun i => primitiveRoots i R
by_cases hn : n = 0
no goals
case neg
M : Type ?u.3642802
N : Type ?u.3642805
G : Type ?u.3642808
R : Type u_1
S : Type ?u.3642814
F : Type ?u.3642817
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
hn : ¬n = 0
⊢ nthRootsFinset n R = Finset.biUnion (Nat.divisors n) fun i => primitiveRoots i R
exact nthRoots_one_eq_biUnion_primitiveRoots' (n := ⟨n, Nat.pos_of_ne_zero hn⟩) h
no goals
case pos
M : Type ?u.3642802
N : Type ?u.3642805
G : Type ?u.3642808
R : Type u_1
S : Type ?u.3642814
F : Type ?u.3642817
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
hn : n = 0
⊢ nthRootsFinset n R = Finset.biUnion (Nat.divisors n) fun i => primitiveRoots i R
simp [hn]