case pos
M : Type ?u.3633248
N : Type ?u.3633251
G : Type ?u.3633254
R : Type u_1
S : Type ?u.3633260
F : Type ?u.3633263
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : k = 0
⊢ card (primitiveRoots k R) = φ k

case neg
M : Type ?u.3633248
N : Type ?u.3633251
G : Type ?u.3633254
R : Type u_1
S : Type ?u.3633260
F : Type ?u.3633263
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
⊢ card (primitiveRoots k R) = φ k
M : Type ?u.3633248
N : Type ?u.3633251
G : Type ?u.3633254
R : Type u_1
S : Type ?u.3633260
F : Type ?u.3633263
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
⊢ card (primitiveRoots k R) = φ k
by_cases h0 : k = 0
case neg
M : Type ?u.3633248
N : Type ?u.3633251
G : Type ?u.3633254
R : Type u_1
S : Type ?u.3633260
F : Type ?u.3633263
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
⊢ φ k = card (primitiveRoots k R)
case neg
M : Type ?u.3633248
N : Type ?u.3633251
G : Type ?u.3633254
R : Type u_1
S : Type ?u.3633260
F : Type ?u.3633263
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
⊢ card (primitiveRoots k R) = φ k
symm
case neg.refine'_1
M : Type ?u.3633248
N : Type ?u.3633251
G : Type ?u.3633254
R : Type u_1
S : Type ?u.3633260
F : Type ?u.3633263
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
⊢ ∀ (a : ℕ) (ha : a ∈ filter (Nat.coprime k) (range k)), (fun i x => ζ ^ i) a ha ∈ primitiveRoots k R

case neg.refine'_2
M : Type ?u.3633248
N : Type ?u.3633251
G : Type ?u.3633254
R : Type u_1
S : Type ?u.3633260
F : Type ?u.3633263
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
⊢ ∀ (a b : ℕ) (ha : a ∈ filter (Nat.coprime k) (range k)) (hb : b ∈ filter (Nat.coprime k) (range k)),
    (fun i x => ζ ^ i) a ha = (fun i x => ζ ^ i) b hb → a = b

case neg.refine'_3
M : Type ?u.3633248
N : Type ?u.3633251
G : Type ?u.3633254
R : Type u_1
S : Type ?u.3633260
F : Type ?u.3633263
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
⊢ ∀ (b : R), b ∈ primitiveRoots k R → ∃ a ha, (fun i x => ζ ^ i) a ha = b
case neg
M : Type ?u.3633248
N : Type ?u.3633251
G : Type ?u.3633254
R : Type u_1
S : Type ?u.3633260
F : Type ?u.3633263
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
⊢ φ k = card (primitiveRoots k R)
refine' Finset.card_congr (fun i _ => ζ ^ i) _ _ _
no goals
case pos
M : Type ?u.3633248
N : Type ?u.3633251
G : Type ?u.3633254
R : Type u_1
S : Type ?u.3633260
F : Type ?u.3633263
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : k = 0
⊢ card (primitiveRoots k R) = φ k
simp [h0]
case neg.refine'_1
M : Type ?u.3633248
N : Type ?u.3633251
G : Type ?u.3633254
R : Type u_1
S : Type ?u.3633260
F : Type ?u.3633263
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
⊢ ∀ (a : ℕ), a < k → Nat.coprime k a → ζ ^ a ∈ primitiveRoots k R
case neg.refine'_1
M : Type ?u.3633248
N : Type ?u.3633251
G : Type ?u.3633254
R : Type u_1
S : Type ?u.3633260
F : Type ?u.3633263
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
⊢ ∀ (a : ℕ) (ha : a ∈ filter (Nat.coprime k) (range k)), (fun i x => ζ ^ i) a ha ∈ primitiveRoots k R
simp only [true_and_iff, and_imp, mem_filter, mem_range, mem_univ]
case neg.refine'_1
M : Type ?u.3633248
N : Type ?u.3633251
G : Type ?u.3633254
R : Type u_1
S : Type ?u.3633260
F : Type ?u.3633263
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
i : ℕ
hi : Nat.coprime k i
⊢ ζ ^ i ∈ primitiveRoots k R
case neg.refine'_1
M : Type ?u.3633248
N : Type ?u.3633251
G : Type ?u.3633254
R : Type u_1
S : Type ?u.3633260
F : Type ?u.3633263
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
⊢ ∀ (a : ℕ), a < k → Nat.coprime k a → ζ ^ a ∈ primitiveRoots k R
rintro i - hi
case neg.refine'_1
M : Type ?u.3633248
N : Type ?u.3633251
G : Type ?u.3633254
R : Type u_1
S : Type ?u.3633260
F : Type ?u.3633263
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
i : ℕ
hi : Nat.coprime k i
⊢ IsPrimitiveRoot (ζ ^ i) k
case neg.refine'_1
M : Type ?u.3633248
N : Type ?u.3633251
G : Type ?u.3633254
R : Type u_1
S : Type ?u.3633260
F : Type ?u.3633263
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
i : ℕ
hi : Nat.coprime k i
⊢ ζ ^ i ∈ primitiveRoots k R
rw [mem_primitiveRoots (Nat.pos_of_ne_zero h0)]
no goals
case neg.refine'_1
M : Type ?u.3633248
N : Type ?u.3633251
G : Type ?u.3633254
R : Type u_1
S : Type ?u.3633260
F : Type ?u.3633263
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
i : ℕ
hi : Nat.coprime k i
⊢ IsPrimitiveRoot (ζ ^ i) k
exact h.pow_of_coprime i hi.symm
case neg.refine'_2
M : Type ?u.3633248
N : Type ?u.3633251
G : Type ?u.3633254
R : Type u_1
S : Type ?u.3633260
F : Type ?u.3633263
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
⊢ ∀ (a b : ℕ), a < k → Nat.coprime k a → b < k → Nat.coprime k b → ζ ^ a = ζ ^ b → a = b
case neg.refine'_2
M : Type ?u.3633248
N : Type ?u.3633251
G : Type ?u.3633254
R : Type u_1
S : Type ?u.3633260
F : Type ?u.3633263
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
⊢ ∀ (a b : ℕ) (ha : a ∈ filter (Nat.coprime k) (range k)) (hb : b ∈ filter (Nat.coprime k) (range k)),
    (fun i x => ζ ^ i) a ha = (fun i x => ζ ^ i) b hb → a = b
simp only [true_and_iff, and_imp, mem_filter, mem_range, mem_univ]
case neg.refine'_2
M : Type ?u.3633248
N : Type ?u.3633251
G : Type ?u.3633254
R : Type u_1
S : Type ?u.3633260
F : Type ?u.3633263
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
i j : ℕ
hi : i < k
hj : j < k
H : ζ ^ i = ζ ^ j
⊢ i = j
case neg.refine'_2
M : Type ?u.3633248
N : Type ?u.3633251
G : Type ?u.3633254
R : Type u_1
S : Type ?u.3633260
F : Type ?u.3633263
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
⊢ ∀ (a b : ℕ), a < k → Nat.coprime k a → b < k → Nat.coprime k b → ζ ^ a = ζ ^ b → a = b
rintro i j hi - hj - H
no goals
case neg.refine'_2
M : Type ?u.3633248
N : Type ?u.3633251
G : Type ?u.3633254
R : Type u_1
S : Type ?u.3633260
F : Type ?u.3633263
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
i j : ℕ
hi : i < k
hj : j < k
H : ζ ^ i = ζ ^ j
⊢ i = j
exact h.pow_inj hi hj H
case neg.refine'_3
M : Type ?u.3633248
N : Type ?u.3633251
G : Type ?u.3633254
R : Type u_1
S : Type ?u.3633260
F : Type ?u.3633263
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
⊢ ∀ (b : R), b ∈ primitiveRoots k R → ∃ a, (a < k ∧ Nat.coprime k a) ∧ ζ ^ a = b
case neg.refine'_3
M : Type ?u.3633248
N : Type ?u.3633251
G : Type ?u.3633254
R : Type u_1
S : Type ?u.3633260
F : Type ?u.3633263
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
⊢ ∀ (b : R), b ∈ primitiveRoots k R → ∃ a ha, (fun i x => ζ ^ i) a ha = b
simp only [exists_prop, true_and_iff, mem_filter, mem_range, mem_univ]
case neg.refine'_3
M : Type ?u.3633248
N : Type ?u.3633251
G : Type ?u.3633254
R : Type u_1
S : Type ?u.3633260
F : Type ?u.3633263
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
ξ : R
hξ : ξ ∈ primitiveRoots k R
⊢ ∃ a, (a < k ∧ Nat.coprime k a) ∧ ζ ^ a = ξ
case neg.refine'_3
M : Type ?u.3633248
N : Type ?u.3633251
G : Type ?u.3633254
R : Type u_1
S : Type ?u.3633260
F : Type ?u.3633263
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
⊢ ∀ (b : R), b ∈ primitiveRoots k R → ∃ a, (a < k ∧ Nat.coprime k a) ∧ ζ ^ a = b
intro ξ hξ
case neg.refine'_3
M : Type ?u.3633248
N : Type ?u.3633251
G : Type ?u.3633254
R : Type u_1
S : Type ?u.3633260
F : Type ?u.3633263
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
ξ : R
hξ : ∃ i, i < k ∧ Nat.coprime i k ∧ ζ ^ i = ξ
⊢ ∃ a, (a < k ∧ Nat.coprime k a) ∧ ζ ^ a = ξ
case neg.refine'_3
M : Type ?u.3633248
N : Type ?u.3633251
G : Type ?u.3633254
R : Type u_1
S : Type ?u.3633260
F : Type ?u.3633263
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
ξ : R
hξ : ξ ∈ primitiveRoots k R
⊢ ∃ a, (a < k ∧ Nat.coprime k a) ∧ ζ ^ a = ξ
rw [mem_primitiveRoots (Nat.pos_of_ne_zero h0),
  h.isPrimitiveRoot_iff (Nat.pos_of_ne_zero h0)] at hξ
case neg.refine'_3.intro.intro.intro
M : Type ?u.3633248
N : Type ?u.3633251
G : Type ?u.3633254
R : Type u_1
S : Type ?u.3633260
F : Type ?u.3633263
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
ξ : R
i : ℕ
hin : i < k
hi : Nat.coprime i k
H : ζ ^ i = ξ
⊢ ∃ a, (a < k ∧ Nat.coprime k a) ∧ ζ ^ a = ξ
case neg.refine'_3
M : Type ?u.3633248
N : Type ?u.3633251
G : Type ?u.3633254
R : Type u_1
S : Type ?u.3633260
F : Type ?u.3633263
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
ξ : R
hξ : ∃ i, i < k ∧ Nat.coprime i k ∧ ζ ^ i = ξ
⊢ ∃ a, (a < k ∧ Nat.coprime k a) ∧ ζ ^ a = ξ
rcases hξ with ⟨i, hin, hi, H⟩
no goals
case neg.refine'_3.intro.intro.intro
M : Type ?u.3633248
N : Type ?u.3633251
G : Type ?u.3633254
R : Type u_1
S : Type ?u.3633260
F : Type ?u.3633263
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k✝ l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h✝ : IsPrimitiveRoot ζ✝ k✝
inst✝ : IsDomain R
ζ : R
k : ℕ
h : IsPrimitiveRoot ζ k
h0 : ¬k = 0
ξ : R
i : ℕ
hin : i < k
hi : Nat.coprime i k
H : ζ ^ i = ξ
⊢ ∃ a, (a < k ∧ Nat.coprime k a) ∧ ζ ^ a = ξ
exact ⟨i, ⟨hin, hi.symm⟩, H⟩