M : Type ?u.3637929
N : Type ?u.3637932
G : Type ?u.3637935
R : Type u_1
S : Type ?u.3637941
F : Type ?u.3637944
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
⊢ (Finset.biUnion (Nat.divisors ↑n) fun i => primitiveRoots i R) = nthRootsFinset (↑n) R
M : Type ?u.3637929
N : Type ?u.3637932
G : Type ?u.3637935
R : Type u_1
S : Type ?u.3637941
F : Type ?u.3637944
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
symm
case h
M : Type ?u.3637929
N : Type ?u.3637932
G : Type ?u.3637935
R : Type u_1
S : Type ?u.3637941
F : Type ?u.3637944
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
⊢ (Finset.biUnion (Nat.divisors ↑n) fun i => primitiveRoots i R) ⊆ nthRootsFinset (↑n) R

case h₂
M : Type ?u.3637929
N : Type ?u.3637932
G : Type ?u.3637935
R : Type u_1
S : Type ?u.3637941
F : Type ?u.3637944
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
⊢ card (nthRootsFinset (↑n) R) ≤ card (Finset.biUnion (Nat.divisors ↑n) fun i => primitiveRoots i R)
M : Type ?u.3637929
N : Type ?u.3637932
G : Type ?u.3637935
R : Type u_1
S : Type ?u.3637941
F : Type ?u.3637944
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
⊢ (Finset.biUnion (Nat.divisors ↑n) fun i => primitiveRoots i R) = nthRootsFinset (↑n) R
apply Finset.eq_of_subset_of_card_le
case h
M : Type ?u.3637929
N : Type ?u.3637932
G : Type ?u.3637935
R : Type u_1
S : Type ?u.3637941
F : Type ?u.3637944
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
x : R
⊢ (x ∈ Finset.biUnion (Nat.divisors ↑n) fun i => primitiveRoots i R) → x ∈ nthRootsFinset (↑n) R
case h
M : Type ?u.3637929
N : Type ?u.3637932
G : Type ?u.3637935
R : Type u_1
S : Type ?u.3637941
F : Type ?u.3637944
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
⊢ (Finset.biUnion (Nat.divisors ↑n) fun i => primitiveRoots i R) ⊆ nthRootsFinset (↑n) R
intro x
case h
M : Type ?u.3637929
N : Type ?u.3637932
G : Type ?u.3637935
R : Type u_1
S : Type ?u.3637941
F : Type ?u.3637944
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
x : R
⊢ (∃ a, a ∣ ↑n ∧ x ∈ primitiveRoots a R) → x ^ ↑n = 1
case h
M : Type ?u.3637929
N : Type ?u.3637932
G : Type ?u.3637935
R : Type u_1
S : Type ?u.3637941
F : Type ?u.3637944
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
x : R
⊢ (x ∈ Finset.biUnion (Nat.divisors ↑n) fun i => primitiveRoots i R) → x ∈ nthRootsFinset (↑n) R
simp only [nthRootsFinset, ← Multiset.toFinset_eq (nthRoots_nodup h), exists_prop,
  Finset.mem_biUnion, Finset.mem_filter, Finset.mem_range, mem_nthRoots, Finset.mem_mk,
  Nat.mem_divisors, and_true_iff, Ne.def, PNat.ne_zero, PNat.pos, not_false_iff]
case h.intro.intro.intro
M : Type ?u.3637929
N : Type ?u.3637932
G : Type ?u.3637935
R : Type u_1
S : Type ?u.3637941
F : Type ?u.3637944
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
x : R
a : ℕ
ha : x ∈ primitiveRoots a R
d : ℕ
hd : ↑n = a * d
⊢ x ^ ↑n = 1
case h
M : Type ?u.3637929
N : Type ?u.3637932
G : Type ?u.3637935
R : Type u_1
S : Type ?u.3637941
F : Type ?u.3637944
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
x : R
⊢ (∃ a, a ∣ ↑n ∧ x ∈ primitiveRoots a R) → x ^ ↑n = 1
rintro ⟨a, ⟨d, hd⟩, ha⟩
case h.intro.intro.intro
M : Type ?u.3637929
N : Type ?u.3637932
G : Type ?u.3637935
R : Type u_1
S : Type ?u.3637941
F : Type ?u.3637944
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
x : R
a : ℕ
ha : x ∈ primitiveRoots a R
d : ℕ
hd : ↑n = a * d
hazero : 0 < a
⊢ x ^ ↑n = 1
case h.intro.intro.intro
M : Type ?u.3637929
N : Type ?u.3637932
G : Type ?u.3637935
R : Type u_1
S : Type ?u.3637941
F : Type ?u.3637944
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
x : R
a : ℕ
ha : x ∈ primitiveRoots a R
d : ℕ
hd : ↑n = a * d
⊢ x ^ ↑n = 1
have hazero : 0 < a := by
  contrapose! hd with ha0
  simp_all only [nonpos_iff_eq_zero, MulZeroClass.zero_mul]
  exact n.ne_zero
case h.intro.intro.intro
M : Type ?u.3637929
N : Type ?u.3637932
G : Type ?u.3637935
R : Type u_1
S : Type ?u.3637941
F : Type ?u.3637944
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
x : R
a : ℕ
ha : IsPrimitiveRoot x a
d : ℕ
hd : ↑n = a * d
hazero : 0 < a
⊢ x ^ ↑n = 1
case h.intro.intro.intro
M : Type ?u.3637929
N : Type ?u.3637932
G : Type ?u.3637935
R : Type u_1
S : Type ?u.3637941
F : Type ?u.3637944
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
x : R
a : ℕ
ha : x ∈ primitiveRoots a R
d : ℕ
hd : ↑n = a * d
hazero : 0 < a
⊢ x ^ ↑n = 1
rw [mem_primitiveRoots hazero] at ha
no goals
case h.intro.intro.intro
M : Type ?u.3637929
N : Type ?u.3637932
G : Type ?u.3637935
R : Type u_1
S : Type ?u.3637941
F : Type ?u.3637944
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
x : R
a : ℕ
ha : IsPrimitiveRoot x a
d : ℕ
hd : ↑n = a * d
hazero : 0 < a
⊢ x ^ ↑n = 1
rw [hd, pow_mul, ha.pow_eq_one, one_pow]
M : Type ?u.3637929
N : Type ?u.3637932
G : Type ?u.3637935
R : Type u_1
S : Type ?u.3637941
F : Type ?u.3637944
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
x : R
a : ℕ
ha : x ∈ primitiveRoots a R
d : ℕ
ha0 : a ≤ 0
⊢ ↑n ≠ a * d
M : Type ?u.3637929
N : Type ?u.3637932
G : Type ?u.3637935
R : Type u_1
S : Type ?u.3637941
F : Type ?u.3637944
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
x : R
a : ℕ
ha : x ∈ primitiveRoots a R
d : ℕ
hd : ↑n = a * d
⊢ 0 < a
contrapose! hd with ha0
M : Type ?u.3637929
N : Type ?u.3637932
G : Type ?u.3637935
R : Type u_1
S : Type ?u.3637941
F : Type ?u.3637944
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
inst✝ : IsDomain R
ζ : R
n : ℕ+
x : R
a d : ℕ
h✝ : IsPrimitiveRoot ζ✝ k
h : IsPrimitiveRoot ζ ↑n
ha : x ∈ primitiveRoots 0 R
ha0 : a = 0
⊢ ↑n ≠ 0
M : Type ?u.3637929
N : Type ?u.3637932
G : Type ?u.3637935
R : Type u_1
S : Type ?u.3637941
F : Type ?u.3637944
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
x : R
a : ℕ
ha : x ∈ primitiveRoots a R
d : ℕ
ha0 : a ≤ 0
⊢ ↑n ≠ a * d
simp_all only [nonpos_iff_eq_zero, MulZeroClass.zero_mul]
no goals
M : Type ?u.3637929
N : Type ?u.3637932
G : Type ?u.3637935
R : Type u_1
S : Type ?u.3637941
F : Type ?u.3637944
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
inst✝ : IsDomain R
ζ : R
n : ℕ+
x : R
a d : ℕ
h✝ : IsPrimitiveRoot ζ✝ k
h : IsPrimitiveRoot ζ ↑n
ha : x ∈ primitiveRoots 0 R
ha0 : a = 0
⊢ ↑n ≠ 0
exact n.ne_zero
case h₂.a
M : Type ?u.3637929
N : Type ?u.3637932
G : Type ?u.3637935
R : Type u_1
S : Type ?u.3637941
F : Type ?u.3637944
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
⊢ card (nthRootsFinset (↑n) R) = card (Finset.biUnion (Nat.divisors ↑n) fun i => primitiveRoots i R)
case h₂
M : Type ?u.3637929
N : Type ?u.3637932
G : Type ?u.3637935
R : Type u_1
S : Type ?u.3637941
F : Type ?u.3637944
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
⊢ card (nthRootsFinset (↑n) R) ≤ card (Finset.biUnion (Nat.divisors ↑n) fun i => primitiveRoots i R)
apply le_of_eq
case h₂.a
M : Type ?u.3637929
N : Type ?u.3637932
G : Type ?u.3637935
R : Type u_1
S : Type ?u.3637941
F : Type ?u.3637944
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
⊢ ↑n = ∑ u in Nat.divisors ↑n, card (primitiveRoots u R)

case h₂.a
M : Type ?u.3637929
N : Type ?u.3637932
G : Type ?u.3637935
R : Type u_1
S : Type ?u.3637941
F : Type ?u.3637944
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
⊢ ∀ (x : ℕ),
    x ∈ Nat.divisors ↑n → ∀ (y : ℕ), y ∈ Nat.divisors ↑n → x ≠ y → Disjoint (primitiveRoots x R) (primitiveRoots y R)
case h₂.a
M : Type ?u.3637929
N : Type ?u.3637932
G : Type ?u.3637935
R : Type u_1
S : Type ?u.3637941
F : Type ?u.3637944
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
⊢ card (nthRootsFinset (↑n) R) = card (Finset.biUnion (Nat.divisors ↑n) fun i => primitiveRoots i R)
rw [h.card_nthRootsFinset, Finset.card_biUnion]
case h₂.a
M : Type ?u.3637929
N : Type ?u.3637932
G : Type ?u.3637935
R : Type u_1
S : Type ?u.3637941
F : Type ?u.3637944
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
⊢ Finset.sum (Nat.divisors ↑n) φ = ∑ u in Nat.divisors ↑n, card (primitiveRoots u R)
case h₂.a
M : Type ?u.3637929
N : Type ?u.3637932
G : Type ?u.3637935
R : Type u_1
S : Type ?u.3637941
F : Type ?u.3637944
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
⊢ ↑n = ∑ u in Nat.divisors ↑n, card (primitiveRoots u R)
nth_rw 1 [← Nat.sum_totient n]
case h₂.a
M : Type ?u.3637929
N : Type ?u.3637932
G : Type ?u.3637935
R : Type u_1
S : Type ?u.3637941
F : Type ?u.3637944
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
⊢ ∀ (x : ℕ), x ∈ Nat.divisors ↑n → φ x = card (primitiveRoots x R)
case h₂.a
M : Type ?u.3637929
N : Type ?u.3637932
G : Type ?u.3637935
R : Type u_1
S : Type ?u.3637941
F : Type ?u.3637944
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
⊢ Finset.sum (Nat.divisors ↑n) φ = ∑ u in Nat.divisors ↑n, card (primitiveRoots u R)
refine' sum_congr rfl _
case h₂.a
M : Type ?u.3637929
N : Type ?u.3637932
G : Type ?u.3637935
R : Type u_1
S : Type ?u.3637941
F : Type ?u.3637944
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
⊢ ∀ (x : ℕ), x ∣ ↑n ∧ ↑n ≠ 0 → φ x = card (primitiveRoots x R)
case h₂.a
M : Type ?u.3637929
N : Type ?u.3637932
G : Type ?u.3637935
R : Type u_1
S : Type ?u.3637941
F : Type ?u.3637944
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
⊢ ∀ (x : ℕ), x ∈ Nat.divisors ↑n → φ x = card (primitiveRoots x R)
simp only [Nat.mem_divisors]
case h₂.a.intro.intro
M : Type ?u.3637929
N : Type ?u.3637932
G : Type ?u.3637935
R : Type u_1
S : Type ?u.3637941
F : Type ?u.3637944
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
k d : ℕ
hd : ↑n = k * d
⊢ φ k = card (primitiveRoots k R)
case h₂.a
M : Type ?u.3637929
N : Type ?u.3637932
G : Type ?u.3637935
R : Type u_1
S : Type ?u.3637941
F : Type ?u.3637944
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
⊢ ∀ (x : ℕ), x ∣ ↑n ∧ ↑n ≠ 0 → φ x = card (primitiveRoots x R)
rintro k ⟨⟨d, hd⟩, -⟩
case h₂.a.intro.intro
M : Type ?u.3637929
N : Type ?u.3637932
G : Type ?u.3637935
R : Type u_1
S : Type ?u.3637941
F : Type ?u.3637944
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
k d : ℕ
hd : ↑n = d * k
⊢ φ k = card (primitiveRoots k R)
case h₂.a.intro.intro
M : Type ?u.3637929
N : Type ?u.3637932
G : Type ?u.3637935
R : Type u_1
S : Type ?u.3637941
F : Type ?u.3637944
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
k d : ℕ
hd : ↑n = k * d
⊢ φ k = card (primitiveRoots k R)
rw [mul_comm] at hd
no goals
case h₂.a.intro.intro
M : Type ?u.3637929
N : Type ?u.3637932
G : Type ?u.3637935
R : Type u_1
S : Type ?u.3637941
F : Type ?u.3637944
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
k d : ℕ
hd : ↑n = d * k
⊢ φ k = card (primitiveRoots k R)
rw [(h.pow n.pos hd).card_primitiveRoots]
case h₂.a
M : Type ?u.3637929
N : Type ?u.3637932
G : Type ?u.3637935
R : Type u_1
S : Type ?u.3637941
F : Type ?u.3637944
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
i : ℕ
a✝¹ : i ∈ Nat.divisors ↑n
j : ℕ
a✝ : j ∈ Nat.divisors ↑n
hdiff : i ≠ j
⊢ Disjoint (primitiveRoots i R) (primitiveRoots j R)
case h₂.a
M : Type ?u.3637929
N : Type ?u.3637932
G : Type ?u.3637935
R : Type u_1
S : Type ?u.3637941
F : Type ?u.3637944
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
⊢ ∀ (x : ℕ),
    x ∈ Nat.divisors ↑n → ∀ (y : ℕ), y ∈ Nat.divisors ↑n → x ≠ y → Disjoint (primitiveRoots x R) (primitiveRoots y R)
intro i _ j _ hdiff
no goals
case h₂.a
M : Type ?u.3637929
N : Type ?u.3637932
G : Type ?u.3637935
R : Type u_1
S : Type ?u.3637941
F : Type ?u.3637944
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
i : ℕ
a✝¹ : i ∈ Nat.divisors ↑n
j : ℕ
a✝ : j ∈ Nat.divisors ↑n
hdiff : i ≠ j
⊢ Disjoint (primitiveRoots i R) (primitiveRoots j R)
exact disjoint hdiff