R✝ : Type ?u.35090
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : ℕ
inst✝ : CharP R p
hp : p ≠ 2
⊢ ∏ μ in primitiveRoots 2 R, (X - ↑C μ) = X + 1
R✝ : Type ?u.35090
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : ℕ
inst✝ : CharP R p
hp : p ≠ 2
⊢ cyclotomic' 2 R = X + 1
rw [cyclotomic']
R✝ : Type ?u.35090
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : ℕ
inst✝ : CharP R p
hp : p ≠ 2
prim_root_two : primitiveRoots 2 R = {-1}
⊢ ∏ μ in primitiveRoots 2 R, (X - ↑C μ) = X + 1
R✝ : Type ?u.35090
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : ℕ
inst✝ : CharP R p
hp : p ≠ 2
⊢ ∏ μ in primitiveRoots 2 R, (X - ↑C μ) = X + 1
have prim_root_two : primitiveRoots 2 R = {(-1 : R)} := by
  simp only [Finset.eq_singleton_iff_unique_mem, mem_primitiveRoots two_pos]
  exact ⟨IsPrimitiveRoot.neg_one p hp, fun x => IsPrimitiveRoot.eq_neg_one_of_two_right⟩
no goals
R✝ : Type ?u.35090
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : ℕ
inst✝ : CharP R p
hp : p ≠ 2
prim_root_two : primitiveRoots 2 R = {-1}
⊢ ∏ μ in primitiveRoots 2 R, (X - ↑C μ) = X + 1
simp only [prim_root_two, Finset.prod_singleton, RingHom.map_neg, RingHom.map_one, sub_neg_eq_add]
R✝ : Type ?u.35090
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : ℕ
inst✝ : CharP R p
hp : p ≠ 2
⊢ IsPrimitiveRoot (-1) 2 ∧ ∀ (x : R), IsPrimitiveRoot x 2 → x = -1
R✝ : Type ?u.35090
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : ℕ
inst✝ : CharP R p
hp : p ≠ 2
⊢ primitiveRoots 2 R = {-1}
simp only [Finset.eq_singleton_iff_unique_mem, mem_primitiveRoots two_pos]
no goals
R✝ : Type ?u.35090
inst✝⁴ : CommRing R✝
inst✝³ : IsDomain R✝
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : ℕ
inst✝ : CharP R p
hp : p ≠ 2
⊢ IsPrimitiveRoot (-1) 2 ∧ ∀ (x : R), IsPrimitiveRoot x 2 → x = -1
exact ⟨IsPrimitiveRoot.neg_one p hp, fun x => IsPrimitiveRoot.eq_neg_one_of_two_right⟩