R : Type u
S : Type ?u.60633
inst✝ : Semiring R
n : ℕ
hn : n ≠ 0
✝ : Nontrivial R
⊢ Monic (∑ i in range n, X ^ i)
R : Type u
S : Type ?u.60633
inst✝ : Semiring R
n : ℕ
hn : n ≠ 0
⊢ Monic (∑ i in range n, X ^ i)
nontriviality R
R : Type u
S : Type ?u.60633
inst✝ : Semiring R
n : ℕ
hn : n ≠ 0
✝ : Nontrivial R
⊢ 0 < natDegree X
R : Type u
S : Type ?u.60633
inst✝ : Semiring R
n : ℕ
hn : n ≠ 0
✝ : Nontrivial R
⊢ Monic (∑ i in range n, X ^ i)
apply monic_X.geom_sum _ hn
no goals
R : Type u
S : Type ?u.60633
inst✝ : Semiring R
n : ℕ
hn : n ≠ 0
✝ : Nontrivial R
⊢ 0 < natDegree X
simp only [natDegree_X, zero_lt_one]