R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
✝ : Nontrivial R
⊢ P = cyclotomic n R ↔ P * ∏ i in Nat.properDivisors n, cyclotomic i R = X ^ n - 1
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
⊢ P = cyclotomic n R ↔ P * ∏ i in Nat.properDivisors n, cyclotomic i R = X ^ n - 1
nontriviality R
case refine'_1
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
✝ : Nontrivial R
hcycl : P = cyclotomic n R
⊢ P * ∏ i in Nat.properDivisors n, cyclotomic i R = X ^ n - 1

case refine'_2
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
✝ : Nontrivial R
hP : P * ∏ i in Nat.properDivisors n, cyclotomic i R = X ^ n - 1
⊢ P = cyclotomic n R
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
✝ : Nontrivial R
⊢ P = cyclotomic n R ↔ P * ∏ i in Nat.properDivisors n, cyclotomic i R = X ^ n - 1
refine' ⟨fun hcycl => _, fun hP => _⟩
no goals
case refine'_1
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
✝ : Nontrivial R
hcycl : P = cyclotomic n R
⊢ P * ∏ i in Nat.properDivisors n, cyclotomic i R = X ^ n - 1
rw [hcycl, ← prod_cyclotomic_eq_X_pow_sub_one hpos R, ← Nat.cons_self_properDivisors hpos.ne',
  Finset.prod_cons]
case refine'_2
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
✝ : Nontrivial R
hP : P * ∏ i in Nat.properDivisors n, cyclotomic i R = X ^ n - 1
prod_monic : Monic (∏ i in Nat.properDivisors n, cyclotomic i R)
⊢ P = cyclotomic n R
case refine'_2
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
✝ : Nontrivial R
hP : P * ∏ i in Nat.properDivisors n, cyclotomic i R = X ^ n - 1
⊢ P = cyclotomic n R
have prod_monic : (∏ i in Nat.properDivisors n, cyclotomic i R).Monic := by
  apply monic_prod_of_monic
  intro i _
  exact cyclotomic.monic i R
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
✝ : Nontrivial R
hP : P * ∏ i in Nat.properDivisors n, cyclotomic i R = X ^ n - 1
prod_monic : Monic (∏ i in Nat.properDivisors n, cyclotomic i R)
⊢ 0 + (∏ i in Nat.properDivisors n, cyclotomic i R) * P = X ^ n - 1 ∧
    degree 0 < degree (∏ i in Nat.properDivisors n, cyclotomic i R)
case refine'_2
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
✝ : Nontrivial R
hP : P * ∏ i in Nat.properDivisors n, cyclotomic i R = X ^ n - 1
prod_monic : Monic (∏ i in Nat.properDivisors n, cyclotomic i R)
⊢ P = cyclotomic n R
rw [@cyclotomic_eq_X_pow_sub_one_div R _ _ hpos, (div_modByMonic_unique P 0 prod_monic _).1]
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
✝ : Nontrivial R
hP : P * ∏ i in Nat.properDivisors n, cyclotomic i R = X ^ n - 1
prod_monic : Monic (∏ i in Nat.properDivisors n, cyclotomic i R)
⊢ degree 0 < degree (∏ i in Nat.properDivisors n, cyclotomic i R)
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
✝ : Nontrivial R
hP : P * ∏ i in Nat.properDivisors n, cyclotomic i R = X ^ n - 1
prod_monic : Monic (∏ i in Nat.properDivisors n, cyclotomic i R)
⊢ 0 + (∏ i in Nat.properDivisors n, cyclotomic i R) * P = X ^ n - 1 ∧
    degree 0 < degree (∏ i in Nat.properDivisors n, cyclotomic i R)
refine' ⟨by rwa [zero_add, mul_comm], _⟩
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
✝ : Nontrivial R
hP : P * ∏ i in Nat.properDivisors n, cyclotomic i R = X ^ n - 1
prod_monic : Monic (∏ i in Nat.properDivisors n, cyclotomic i R)
⊢ degree (∏ i in Nat.properDivisors n, cyclotomic i R) ≠ ⊥
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
✝ : Nontrivial R
hP : P * ∏ i in Nat.properDivisors n, cyclotomic i R = X ^ n - 1
prod_monic : Monic (∏ i in Nat.properDivisors n, cyclotomic i R)
⊢ degree 0 < degree (∏ i in Nat.properDivisors n, cyclotomic i R)
rw [degree_zero, bot_lt_iff_ne_bot]
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
✝ : Nontrivial R
hP : P * ∏ i in Nat.properDivisors n, cyclotomic i R = X ^ n - 1
prod_monic : Monic (∏ i in Nat.properDivisors n, cyclotomic i R)
h : degree (∏ i in Nat.properDivisors n, cyclotomic i R) = ⊥
⊢ False
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
✝ : Nontrivial R
hP : P * ∏ i in Nat.properDivisors n, cyclotomic i R = X ^ n - 1
prod_monic : Monic (∏ i in Nat.properDivisors n, cyclotomic i R)
⊢ degree (∏ i in Nat.properDivisors n, cyclotomic i R) ≠ ⊥
intro h
no goals
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
✝ : Nontrivial R
hP : P * ∏ i in Nat.properDivisors n, cyclotomic i R = X ^ n - 1
prod_monic : Monic (∏ i in Nat.properDivisors n, cyclotomic i R)
h : degree (∏ i in Nat.properDivisors n, cyclotomic i R) = ⊥
⊢ False
exact Monic.ne_zero prod_monic (degree_eq_bot.1 h)
case hs
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
✝ : Nontrivial R
hP : P * ∏ i in Nat.properDivisors n, cyclotomic i R = X ^ n - 1
⊢ ∀ (i : ℕ), i ∈ Nat.properDivisors n → Monic (cyclotomic i R)
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
✝ : Nontrivial R
hP : P * ∏ i in Nat.properDivisors n, cyclotomic i R = X ^ n - 1
⊢ Monic (∏ i in Nat.properDivisors n, cyclotomic i R)
apply monic_prod_of_monic
case hs
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
✝ : Nontrivial R
hP : P * ∏ i in Nat.properDivisors n, cyclotomic i R = X ^ n - 1
i : ℕ
a✝ : i ∈ Nat.properDivisors n
⊢ Monic (cyclotomic i R)
case hs
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
✝ : Nontrivial R
hP : P * ∏ i in Nat.properDivisors n, cyclotomic i R = X ^ n - 1
⊢ ∀ (i : ℕ), i ∈ Nat.properDivisors n → Monic (cyclotomic i R)
intro i _
no goals
case hs
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
✝ : Nontrivial R
hP : P * ∏ i in Nat.properDivisors n, cyclotomic i R = X ^ n - 1
i : ℕ
a✝ : i ∈ Nat.properDivisors n
⊢ Monic (cyclotomic i R)
exact cyclotomic.monic i R
no goals
R : Type u_1
inst✝ : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
✝ : Nontrivial R
hP : P * ∏ i in Nat.properDivisors n, cyclotomic i R = X ^ n - 1
prod_monic : Monic (∏ i in Nat.properDivisors n, cyclotomic i R)
⊢ 0 + (∏ i in Nat.properDivisors n, cyclotomic i R) * P = X ^ n - 1
rwa [zero_add, mul_comm]