K✝ : Type ?u.243517
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ cyclotomic' n K =
    (cyclotomic' n K * ∏ x in Nat.properDivisors n, cyclotomic' x K) /ₘ ∏ i in Nat.properDivisors n, cyclotomic' i K
K✝ : Type ?u.243517
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ cyclotomic' n K = (X ^ n - 1) /ₘ ∏ i in Nat.properDivisors n, cyclotomic' i K
rw [← prod_cyclotomic'_eq_X_pow_sub_one hpos h, ← Nat.cons_self_properDivisors hpos.ne',
  Finset.prod_cons]
K✝ : Type ?u.243517
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
prod_monic : Monic (∏ i in Nat.properDivisors n, cyclotomic' i K)
⊢ cyclotomic' n K =
    (cyclotomic' n K * ∏ x in Nat.properDivisors n, cyclotomic' x K) /ₘ ∏ i in Nat.properDivisors n, cyclotomic' i K
K✝ : Type ?u.243517
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ cyclotomic' n K =
    (cyclotomic' n K * ∏ x in Nat.properDivisors n, cyclotomic' x K) /ₘ ∏ i in Nat.properDivisors n, cyclotomic' i K
have prod_monic : (∏ i in Nat.properDivisors n, cyclotomic' i K).Monic := by
  apply monic_prod_of_monic
  intro i _
  exact cyclotomic'.monic i K
K✝ : Type ?u.243517
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
prod_monic : Monic (∏ i in Nat.properDivisors n, cyclotomic' i K)
⊢ 0 + (∏ i in Nat.properDivisors n, cyclotomic' i K) * cyclotomic' n K =
      cyclotomic' n K * ∏ x in Nat.properDivisors n, cyclotomic' x K ∧
    degree 0 < degree (∏ i in Nat.properDivisors n, cyclotomic' i K)
K✝ : Type ?u.243517
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
prod_monic : Monic (∏ i in Nat.properDivisors n, cyclotomic' i K)
⊢ cyclotomic' n K =
    (cyclotomic' n K * ∏ x in Nat.properDivisors n, cyclotomic' x K) /ₘ ∏ i in Nat.properDivisors n, cyclotomic' i K
rw [(div_modByMonic_unique (cyclotomic' n K) 0 prod_monic _).1]
K✝ : Type ?u.243517
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
prod_monic : Monic (∏ i in Nat.properDivisors n, cyclotomic' i K)
⊢ (∏ i in Nat.properDivisors n, cyclotomic' i K) * cyclotomic' n K =
      cyclotomic' n K * ∏ i in Nat.properDivisors n, cyclotomic' i K ∧
    ⊥ < degree (∏ i in Nat.properDivisors n, cyclotomic' i K)
K✝ : Type ?u.243517
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
prod_monic : Monic (∏ i in Nat.properDivisors n, cyclotomic' i K)
⊢ 0 + (∏ i in Nat.properDivisors n, cyclotomic' i K) * cyclotomic' n K =
      cyclotomic' n K * ∏ x in Nat.properDivisors n, cyclotomic' x K ∧
    degree 0 < degree (∏ i in Nat.properDivisors n, cyclotomic' i K)
simp only [degree_zero, zero_add]
K✝ : Type ?u.243517
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
prod_monic : Monic (∏ i in Nat.properDivisors n, cyclotomic' i K)
⊢ ⊥ < degree (∏ i in Nat.properDivisors n, cyclotomic' i K)
K✝ : Type ?u.243517
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
prod_monic : Monic (∏ i in Nat.properDivisors n, cyclotomic' i K)
⊢ (∏ i in Nat.properDivisors n, cyclotomic' i K) * cyclotomic' n K =
      cyclotomic' n K * ∏ i in Nat.properDivisors n, cyclotomic' i K ∧
    ⊥ < degree (∏ i in Nat.properDivisors n, cyclotomic' i K)
refine' ⟨by rw [mul_comm], _⟩
K✝ : Type ?u.243517
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
prod_monic : Monic (∏ i in Nat.properDivisors n, cyclotomic' i K)
⊢ degree (∏ i in Nat.properDivisors n, cyclotomic' i K) ≠ ⊥
K✝ : Type ?u.243517
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
prod_monic : Monic (∏ i in Nat.properDivisors n, cyclotomic' i K)
⊢ ⊥ < degree (∏ i in Nat.properDivisors n, cyclotomic' i K)
rw [bot_lt_iff_ne_bot]
K✝ : Type ?u.243517
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h✝ : IsPrimitiveRoot ζ n
prod_monic : Monic (∏ i in Nat.properDivisors n, cyclotomic' i K)
h : degree (∏ i in Nat.properDivisors n, cyclotomic' i K) = ⊥
⊢ False
K✝ : Type ?u.243517
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
prod_monic : Monic (∏ i in Nat.properDivisors n, cyclotomic' i K)
⊢ degree (∏ i in Nat.properDivisors n, cyclotomic' i K) ≠ ⊥
intro h
no goals
K✝ : Type ?u.243517
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h✝ : IsPrimitiveRoot ζ n
prod_monic : Monic (∏ i in Nat.properDivisors n, cyclotomic' i K)
h : degree (∏ i in Nat.properDivisors n, cyclotomic' i K) = ⊥
⊢ False
exact Monic.ne_zero prod_monic (degree_eq_bot.1 h)
case hs
K✝ : Type ?u.243517
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ ∀ (i : ℕ), i ∈ Nat.properDivisors n → Monic (cyclotomic' i K)
K✝ : Type ?u.243517
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ Monic (∏ i in Nat.properDivisors n, cyclotomic' i K)
apply monic_prod_of_monic
case hs
K✝ : Type ?u.243517
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
i : ℕ
a✝ : i ∈ Nat.properDivisors n
⊢ Monic (cyclotomic' i K)
case hs
K✝ : Type ?u.243517
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ ∀ (i : ℕ), i ∈ Nat.properDivisors n → Monic (cyclotomic' i K)
intro i _
no goals
case hs
K✝ : Type ?u.243517
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
i : ℕ
a✝ : i ∈ Nat.properDivisors n
⊢ Monic (cyclotomic' i K)
exact cyclotomic'.monic i K
no goals
K✝ : Type ?u.243517
inst✝² : Field K✝
K : Type u_1
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
prod_monic : Monic (∏ i in Nat.properDivisors n, cyclotomic' i K)
⊢ (∏ i in Nat.properDivisors n, cyclotomic' i K) * cyclotomic' n K =
    cyclotomic' n K * ∏ i in Nat.properDivisors n, cyclotomic' i K
rw [mul_comm]