R : Type u
S : Type ?u.54680
inst✝ : Semiring R
P : R[X]
hP : Monic P
hdeg : 0 < natDegree P
n : ℕ
hn : n ≠ 0
✝ : Nontrivial R
⊢ Monic (∑ i in range n, P ^ i)
R : Type u
S : Type ?u.54680
inst✝ : Semiring R
P : R[X]
hP : Monic P
hdeg : 0 < natDegree P
n : ℕ
hn : n ≠ 0
⊢ Monic (∑ i in range n, P ^ i)
nontriviality R
case intro
R : Type u
S : Type ?u.54680
inst✝ : Semiring R
P : R[X]
hP : Monic P
hdeg : 0 < natDegree P
✝ : Nontrivial R
n : ℕ
hn : Nat.succ n ≠ 0
⊢ Monic (∑ i in range (Nat.succ n), P ^ i)
R : Type u
S : Type ?u.54680
inst✝ : Semiring R
P : R[X]
hP : Monic P
hdeg : 0 < natDegree P
n : ℕ
hn : n ≠ 0
✝ : Nontrivial R
⊢ Monic (∑ i in range n, P ^ i)
obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hn
case intro
R : Type u
S : Type ?u.54680
inst✝ : Semiring R
P : R[X]
hP : Monic P
hdeg : 0 < natDegree P
✝ : Nontrivial R
n : ℕ
hn : Nat.succ n ≠ 0
⊢ Monic (P ^ n + ∑ i in range n, P ^ i)
case intro
R : Type u
S : Type ?u.54680
inst✝ : Semiring R
P : R[X]
hP : Monic P
hdeg : 0 < natDegree P
✝ : Nontrivial R
n : ℕ
hn : Nat.succ n ≠ 0
⊢ Monic (∑ i in range (Nat.succ n), P ^ i)
rw [geom_sum_succ']
case intro
R : Type u
S : Type ?u.54680
inst✝ : Semiring R
P : R[X]
hP : Monic P
hdeg : 0 < natDegree P
✝ : Nontrivial R
n : ℕ
hn : Nat.succ n ≠ 0
⊢ degree (∑ i in range n, P ^ i) < degree (P ^ n)
case intro
R : Type u
S : Type ?u.54680
inst✝ : Semiring R
P : R[X]
hP : Monic P
hdeg : 0 < natDegree P
✝ : Nontrivial R
n : ℕ
hn : Nat.succ n ≠ 0
⊢ Monic (P ^ n + ∑ i in range n, P ^ i)
refine' (hP.pow _).add_of_left _
case intro
R : Type u
S : Type ?u.54680
inst✝ : Semiring R
P : R[X]
hP : Monic P
hdeg : 0 < natDegree P
✝ : Nontrivial R
n : ℕ
hn : Nat.succ n ≠ 0
⊢ (sup (range n) fun b => degree (P ^ b)) < degree (P ^ n)
case intro
R : Type u
S : Type ?u.54680
inst✝ : Semiring R
P : R[X]
hP : Monic P
hdeg : 0 < natDegree P
✝ : Nontrivial R
n : ℕ
hn : Nat.succ n ≠ 0
⊢ degree (∑ i in range n, P ^ i) < degree (P ^ n)
refine' lt_of_le_of_lt (degree_sum_le _ _) _
case intro
R : Type u
S : Type ?u.54680
inst✝ : Semiring R
P : R[X]
hP : Monic P
hdeg : 0 < natDegree P
✝ : Nontrivial R
n : ℕ
hn : Nat.succ n ≠ 0
⊢ ∀ (b : ℕ), b ∈ range n → degree (P ^ b) < degree (P ^ n)

case intro
R : Type u
S : Type ?u.54680
inst✝ : Semiring R
P : R[X]
hP : Monic P
hdeg : 0 < natDegree P
✝ : Nontrivial R
n : ℕ
hn : Nat.succ n ≠ 0
⊢ ⊥ < degree (P ^ n)
case intro
R : Type u
S : Type ?u.54680
inst✝ : Semiring R
P : R[X]
hP : Monic P
hdeg : 0 < natDegree P
✝ : Nontrivial R
n : ℕ
hn : Nat.succ n ≠ 0
⊢ (sup (range n) fun b => degree (P ^ b)) < degree (P ^ n)
rw [Finset.sup_lt_iff]
case intro
R : Type u
S : Type ?u.54680
inst✝ : Semiring R
P : R[X]
hP : Monic P
hdeg : 0 < natDegree P
✝ : Nontrivial R
n : ℕ
hn : Nat.succ n ≠ 0
⊢ ∀ (b : ℕ), b < n → ↑(natDegree (P ^ b)) < ↑(natDegree (P ^ n))
case intro
R : Type u
S : Type ?u.54680
inst✝ : Semiring R
P : R[X]
hP : Monic P
hdeg : 0 < natDegree P
✝ : Nontrivial R
n : ℕ
hn : Nat.succ n ≠ 0
⊢ ∀ (b : ℕ), b ∈ range n → degree (P ^ b) < degree (P ^ n)
simp only [Finset.mem_range, degree_eq_natDegree (hP.pow _).ne_zero]
case intro
R : Type u
S : Type ?u.54680
inst✝ : Semiring R
P : R[X]
hP : Monic P
hdeg : 0 < natDegree P
✝ : Nontrivial R
n : ℕ
hn : Nat.succ n ≠ 0
⊢ ∀ (b : ℕ), b < n → b * natDegree P < n * natDegree P
case intro
R : Type u
S : Type ?u.54680
inst✝ : Semiring R
P : R[X]
hP : Monic P
hdeg : 0 < natDegree P
✝ : Nontrivial R
n : ℕ
hn : Nat.succ n ≠ 0
⊢ ∀ (b : ℕ), b < n → ↑(natDegree (P ^ b)) < ↑(natDegree (P ^ n))
simp only [Nat.cast_withBot, WithBot.coe_lt_coe, hP.natDegree_pow]
case intro
R : Type u
S : Type ?u.54680
inst✝ : Semiring R
P : R[X]
hP : Monic P
hdeg : 0 < natDegree P
✝ : Nontrivial R
n : ℕ
hn : Nat.succ n ≠ 0
k : ℕ
⊢ k < n → k * natDegree P < n * natDegree P
case intro
R : Type u
S : Type ?u.54680
inst✝ : Semiring R
P : R[X]
hP : Monic P
hdeg : 0 < natDegree P
✝ : Nontrivial R
n : ℕ
hn : Nat.succ n ≠ 0
⊢ ∀ (b : ℕ), b < n → b * natDegree P < n * natDegree P
intro k
no goals
case intro
R : Type u
S : Type ?u.54680
inst✝ : Semiring R
P : R[X]
hP : Monic P
hdeg : 0 < natDegree P
✝ : Nontrivial R
n : ℕ
hn : Nat.succ n ≠ 0
k : ℕ
⊢ k < n → k * natDegree P < n * natDegree P
exact nsmul_lt_nsmul hdeg
case intro
R : Type u
S : Type ?u.54680
inst✝ : Semiring R
P : R[X]
hP : Monic P
hdeg : 0 < natDegree P
✝ : Nontrivial R
n : ℕ
hn : Nat.succ n ≠ 0
⊢ ¬P ^ n = 0
case intro
R : Type u
S : Type ?u.54680
inst✝ : Semiring R
P : R[X]
hP : Monic P
hdeg : 0 < natDegree P
✝ : Nontrivial R
n : ℕ
hn : Nat.succ n ≠ 0
⊢ ⊥ < degree (P ^ n)
rw [bot_lt_iff_ne_bot, Ne.def, degree_eq_bot]
no goals
case intro
R : Type u
S : Type ?u.54680
inst✝ : Semiring R
P : R[X]
hP : Monic P
hdeg : 0 < natDegree P
✝ : Nontrivial R
n : ℕ
hn : Nat.succ n ≠ 0
⊢ ¬P ^ n = 0
exact (hP.pow _).ne_zero