case inl
M : Type ?u.3600187
N : Type ?u.3600190
G : Type ?u.3600193
R : Type u_1
S : Type ?u.3600199
F : Type ?u.3600202
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
hzero : n = 0
⊢ Multiset.Nodup (nthRoots n 1)

case inr
M : Type ?u.3600187
N : Type ?u.3600190
G : Type ?u.3600193
R : Type u_1
S : Type ?u.3600199
F : Type ?u.3600202
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
hpos : n > 0
⊢ Multiset.Nodup (nthRoots n 1)
M : Type ?u.3600187
N : Type ?u.3600190
G : Type ?u.3600193
R : Type u_1
S : Type ?u.3600199
F : Type ?u.3600202
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
⊢ Multiset.Nodup (nthRoots n 1)
cases' Nat.eq_zero_or_pos n with hzero hpos
case inr
M : Type ?u.3600187
N : Type ?u.3600190
G : Type ?u.3600193
R : Type u_1
S : Type ?u.3600199
F : Type ?u.3600202
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
hpos : n > 0
⊢ Multiset.dedup (nthRoots n 1) = nthRoots n 1
case inr
M : Type ?u.3600187
N : Type ?u.3600190
G : Type ?u.3600193
R : Type u_1
S : Type ?u.3600199
F : Type ?u.3600202
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
hpos : n > 0
⊢ Multiset.Nodup (nthRoots n 1)
apply (Multiset.dedup_eq_self (α := R)).1
case inr
M : Type ?u.3600187
N : Type ?u.3600190
G : Type ?u.3600193
R : Type u_1
S : Type ?u.3600199
F : Type ?u.3600202
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
hpos : n > 0
⊢ Multiset.dedup (nthRoots n 1) ≤ nthRoots n 1 ∧ ¬Multiset.dedup (nthRoots n 1) < nthRoots n 1
case inr
M : Type ?u.3600187
N : Type ?u.3600190
G : Type ?u.3600193
R : Type u_1
S : Type ?u.3600199
F : Type ?u.3600202
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
hpos : n > 0
⊢ Multiset.dedup (nthRoots n 1) = nthRoots n 1
rw [eq_iff_le_not_lt]
case inr.left
M : Type ?u.3600187
N : Type ?u.3600190
G : Type ?u.3600193
R : Type u_1
S : Type ?u.3600199
F : Type ?u.3600202
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
hpos : n > 0
⊢ Multiset.dedup (nthRoots n 1) ≤ nthRoots n 1

case inr.right
M : Type ?u.3600187
N : Type ?u.3600190
G : Type ?u.3600193
R : Type u_1
S : Type ?u.3600199
F : Type ?u.3600202
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
hpos : n > 0
⊢ ¬Multiset.dedup (nthRoots n 1) < nthRoots n 1
case inr
M : Type ?u.3600187
N : Type ?u.3600190
G : Type ?u.3600193
R : Type u_1
S : Type ?u.3600199
F : Type ?u.3600202
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
hpos : n > 0
⊢ Multiset.dedup (nthRoots n 1) ≤ nthRoots n 1 ∧ ¬Multiset.dedup (nthRoots n 1) < nthRoots n 1
constructor
no goals
case inl
M : Type ?u.3600187
N : Type ?u.3600190
G : Type ?u.3600193
R : Type u_1
S : Type ?u.3600199
F : Type ?u.3600202
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
hzero : n = 0
⊢ Multiset.Nodup (nthRoots n 1)
simp only [hzero, Multiset.nodup_zero, nthRoots_zero]
no goals
case inr.left
M : Type ?u.3600187
N : Type ?u.3600190
G : Type ?u.3600193
R : Type u_1
S : Type ?u.3600199
F : Type ?u.3600202
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
hpos : n > 0
⊢ Multiset.dedup (nthRoots n 1) ≤ nthRoots n 1
exact Multiset.dedup_le (nthRoots n (1 : R))
case inr.right
M : Type ?u.3600187
N : Type ?u.3600190
G : Type ?u.3600193
R : Type u_1
S : Type ?u.3600199
F : Type ?u.3600202
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
hpos : n > 0
ha : Multiset.dedup (nthRoots n 1) < nthRoots n 1
⊢ False
case inr.right
M : Type ?u.3600187
N : Type ?u.3600190
G : Type ?u.3600193
R : Type u_1
S : Type ?u.3600199
F : Type ?u.3600202
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
hpos : n > 0
⊢ ¬Multiset.dedup (nthRoots n 1) < nthRoots n 1
by_contra ha
case inr.right
M : Type ?u.3600187
N : Type ?u.3600190
G : Type ?u.3600193
R : Type u_1
S : Type ?u.3600199
F : Type ?u.3600202
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
hpos : n > 0
ha : ↑Multiset.card (Multiset.dedup (nthRoots n 1)) < ↑Multiset.card (nthRoots n 1)
⊢ False
case inr.right
M : Type ?u.3600187
N : Type ?u.3600190
G : Type ?u.3600193
R : Type u_1
S : Type ?u.3600199
F : Type ?u.3600202
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
hpos : n > 0
ha : Multiset.dedup (nthRoots n 1) < nthRoots n 1
⊢ False
replace ha := Multiset.card_lt_of_lt ha
case inr.right
M : Type ?u.3600187
N : Type ?u.3600190
G : Type ?u.3600193
R : Type u_1
S : Type ?u.3600199
F : Type ?u.3600202
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
hpos : n > 0
ha : ↑Multiset.card (Multiset.dedup (nthRoots n 1)) < n
⊢ False
case inr.right
M : Type ?u.3600187
N : Type ?u.3600190
G : Type ?u.3600193
R : Type u_1
S : Type ?u.3600199
F : Type ?u.3600202
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
hpos : n > 0
ha : ↑Multiset.card (Multiset.dedup (nthRoots n 1)) < ↑Multiset.card (nthRoots n 1)
⊢ False
rw [card_nthRoots h] at ha
case inr.right
M : Type ?u.3600187
N : Type ?u.3600190
G : Type ?u.3600193
R : Type u_1
S : Type ?u.3600199
F : Type ?u.3600202
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
hpos : n > 0
ha : ↑Multiset.card (Multiset.dedup (nthRoots n 1)) < n
hrw : ↑Multiset.card (Multiset.dedup (nthRoots n 1)) = Fintype.card { x // x ∈ nthRoots n 1 }
⊢ False
case inr.right
M : Type ?u.3600187
N : Type ?u.3600190
G : Type ?u.3600193
R : Type u_1
S : Type ?u.3600199
F : Type ?u.3600202
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
hpos : n > 0
ha : ↑Multiset.card (Multiset.dedup (nthRoots n 1)) < n
⊢ False
have hrw : Multiset.card (nthRoots n (1 : R)).dedup =
    Fintype.card { x // x ∈ nthRoots n (1 : R) } := by
  set fs := (⟨(nthRoots n (1 : R)).dedup, Multiset.nodup_dedup _⟩ : Finset R)
  rw [← Finset.card_mk, Fintype.card_of_subtype fs _]
  intro x
  simp only [Multiset.mem_dedup, Finset.mem_mk]
case inr.right
M : Type ?u.3600187
N : Type ?u.3600190
G : Type ?u.3600193
R : Type u_1
S : Type ?u.3600199
F : Type ?u.3600202
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 ζ ↑(Nat.toPNat' n)
hpos : n > 0
ha : ↑Multiset.card (Multiset.dedup (nthRoots (↑(Nat.toPNat' n)) 1)) < ↑(Nat.toPNat' n)
hrw :
  ↑Multiset.card (Multiset.dedup (nthRoots (↑(Nat.toPNat' n)) 1)) =
    Fintype.card { x // x ∈ nthRoots (↑(Nat.toPNat' n)) 1 }
⊢ False
case inr.right
M : Type ?u.3600187
N : Type ?u.3600190
G : Type ?u.3600193
R : Type u_1
S : Type ?u.3600199
F : Type ?u.3600202
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
hpos : n > 0
ha : ↑Multiset.card (Multiset.dedup (nthRoots n 1)) < n
hrw : ↑Multiset.card (Multiset.dedup (nthRoots n 1)) = Fintype.card { x // x ∈ nthRoots n 1 }
⊢ False
rw [← PNat.toPNat'_coe hpos] at h hrw ha
case inr.right
M : Type ?u.3600187
N : Type ?u.3600190
G : Type ?u.3600193
R : Type u_1
S : Type ?u.3600199
F : Type ?u.3600202
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : n > 0
m : ℕ+ := Nat.toPNat' n
h : IsPrimitiveRoot ζ ↑m
ha : ↑Multiset.card (Multiset.dedup (nthRoots (↑m) 1)) < ↑m
hrw : ↑Multiset.card (Multiset.dedup (nthRoots (↑m) 1)) = Fintype.card { x // x ∈ nthRoots (↑m) 1 }
⊢ False
case inr.right
M : Type ?u.3600187
N : Type ?u.3600190
G : Type ?u.3600193
R : Type u_1
S : Type ?u.3600199
F : Type ?u.3600202
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 ζ ↑(Nat.toPNat' n)
hpos : n > 0
ha : ↑Multiset.card (Multiset.dedup (nthRoots (↑(Nat.toPNat' n)) 1)) < ↑(Nat.toPNat' n)
hrw :
  ↑Multiset.card (Multiset.dedup (nthRoots (↑(Nat.toPNat' n)) 1)) =
    Fintype.card { x // x ∈ nthRoots (↑(Nat.toPNat' n)) 1 }
⊢ False
set m := Nat.toPNat' n
case inr.right
M : Type ?u.3600187
N : Type ?u.3600190
G : Type ?u.3600193
R : Type u_1
S : Type ?u.3600199
F : Type ?u.3600202
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : n > 0
m : ℕ+ := Nat.toPNat' n
h : IsPrimitiveRoot ζ ↑m
ha : ↑m < ↑m
hrw : ↑Multiset.card (Multiset.dedup (nthRoots (↑m) 1)) = Fintype.card { x // x ∈ nthRoots (↑m) 1 }
⊢ False
case inr.right
M : Type ?u.3600187
N : Type ?u.3600190
G : Type ?u.3600193
R : Type u_1
S : Type ?u.3600199
F : Type ?u.3600202
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : n > 0
m : ℕ+ := Nat.toPNat' n
h : IsPrimitiveRoot ζ ↑m
ha : ↑Multiset.card (Multiset.dedup (nthRoots (↑m) 1)) < ↑m
hrw : ↑Multiset.card (Multiset.dedup (nthRoots (↑m) 1)) = Fintype.card { x // x ∈ nthRoots (↑m) 1 }
⊢ False
rw [hrw, ← Fintype.card_congr (rootsOfUnityEquivNthRoots R m), card_rootsOfUnity h] at ha
no goals
case inr.right
M : Type ?u.3600187
N : Type ?u.3600190
G : Type ?u.3600193
R : Type u_1
S : Type ?u.3600199
F : Type ?u.3600202
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k
inst✝ : IsDomain R
ζ : R
n : ℕ
hpos : n > 0
m : ℕ+ := Nat.toPNat' n
h : IsPrimitiveRoot ζ ↑m
ha : ↑m < ↑m
hrw : ↑Multiset.card (Multiset.dedup (nthRoots (↑m) 1)) = Fintype.card { x // x ∈ nthRoots (↑m) 1 }
⊢ False
exact Nat.lt_asymm ha ha
M : Type ?u.3600187
N : Type ?u.3600190
G : Type ?u.3600193
R : Type u_1
S : Type ?u.3600199
F : Type ?u.3600202
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
hpos : n > 0
ha : ↑Multiset.card (Multiset.dedup (nthRoots n 1)) < n
fs : Finset R := { val := Multiset.dedup (nthRoots n 1), nodup := (_ : Multiset.Nodup (Multiset.dedup (nthRoots n 1))) }
⊢ ↑Multiset.card (Multiset.dedup (nthRoots n 1)) = Fintype.card { x // x ∈ nthRoots n 1 }
M : Type ?u.3600187
N : Type ?u.3600190
G : Type ?u.3600193
R : Type u_1
S : Type ?u.3600199
F : Type ?u.3600202
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
hpos : n > 0
ha : ↑Multiset.card (Multiset.dedup (nthRoots n 1)) < n
⊢ ↑Multiset.card (Multiset.dedup (nthRoots n 1)) = Fintype.card { x // x ∈ nthRoots n 1 }
set fs := (⟨(nthRoots n (1 : R)).dedup, Multiset.nodup_dedup _⟩ : Finset R)
M : Type ?u.3600187
N : Type ?u.3600190
G : Type ?u.3600193
R : Type u_1
S : Type ?u.3600199
F : Type ?u.3600202
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
hpos : n > 0
ha : ↑Multiset.card (Multiset.dedup (nthRoots n 1)) < n
fs : Finset R := { val := Multiset.dedup (nthRoots n 1), nodup := (_ : Multiset.Nodup (Multiset.dedup (nthRoots n 1))) }
⊢ ∀ (x : R), x ∈ fs ↔ x ∈ nthRoots n 1
M : Type ?u.3600187
N : Type ?u.3600190
G : Type ?u.3600193
R : Type u_1
S : Type ?u.3600199
F : Type ?u.3600202
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
hpos : n > 0
ha : ↑Multiset.card (Multiset.dedup (nthRoots n 1)) < n
fs : Finset R := { val := Multiset.dedup (nthRoots n 1), nodup := (_ : Multiset.Nodup (Multiset.dedup (nthRoots n 1))) }
⊢ ↑Multiset.card (Multiset.dedup (nthRoots n 1)) = Fintype.card { x // x ∈ nthRoots n 1 }
rw [← Finset.card_mk, Fintype.card_of_subtype fs _]
M : Type ?u.3600187
N : Type ?u.3600190
G : Type ?u.3600193
R : Type u_1
S : Type ?u.3600199
F : Type ?u.3600202
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
hpos : n > 0
ha : ↑Multiset.card (Multiset.dedup (nthRoots n 1)) < n
fs : Finset R := { val := Multiset.dedup (nthRoots n 1), nodup := (_ : Multiset.Nodup (Multiset.dedup (nthRoots n 1))) }
x : R
⊢ x ∈ fs ↔ x ∈ nthRoots n 1
M : Type ?u.3600187
N : Type ?u.3600190
G : Type ?u.3600193
R : Type u_1
S : Type ?u.3600199
F : Type ?u.3600202
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
hpos : n > 0
ha : ↑Multiset.card (Multiset.dedup (nthRoots n 1)) < n
fs : Finset R := { val := Multiset.dedup (nthRoots n 1), nodup := (_ : Multiset.Nodup (Multiset.dedup (nthRoots n 1))) }
⊢ ∀ (x : R), x ∈ fs ↔ x ∈ nthRoots n 1
intro x
no goals
M : Type ?u.3600187
N : Type ?u.3600190
G : Type ?u.3600193
R : Type u_1
S : Type ?u.3600199
F : Type ?u.3600202
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
hpos : n > 0
ha : ↑Multiset.card (Multiset.dedup (nthRoots n 1)) < n
fs : Finset R := { val := Multiset.dedup (nthRoots n 1), nodup := (_ : Multiset.Nodup (Multiset.dedup (nthRoots n 1))) }
x : R
⊢ x ∈ fs ↔ x ∈ nthRoots n 1
simp only [Multiset.mem_dedup, Finset.mem_mk]