R : Type u_1
inst✝ : Semiring R
r✝ : R
f p : R[X]
r : R
⊢ ∀ (n : ℕ) (c : R), c ≠ 0 → natDegree (↑(taylor r) (↑(monomial n) c)) = n
R : Type u_1
inst✝ : Semiring R
r✝ : R
f p : R[X]
r : R
⊢ natDegree (↑(taylor r) p) = natDegree p
refine' map_natDegree_eq_natDegree _ _
R : Type u_1
inst✝ : Semiring R
r✝ : R
f p : R[X]
r : R
✝ : Nontrivial R
⊢ ∀ (n : ℕ) (c : R), c ≠ 0 → natDegree (↑(taylor r) (↑(monomial n) c)) = n
R : Type u_1
inst✝ : Semiring R
r✝ : R
f p : R[X]
r : R
⊢ ∀ (n : ℕ) (c : R), c ≠ 0 → natDegree (↑(taylor r) (↑(monomial n) c)) = n
nontriviality R
R : Type u_1
inst✝ : Semiring R
r✝ : R
f p : R[X]
r : R
✝ : Nontrivial R
n : ℕ
c : R
c0 : c ≠ 0
⊢ natDegree (↑(taylor r) (↑(monomial n) c)) = n
R : Type u_1
inst✝ : Semiring R
r✝ : R
f p : R[X]
r : R
✝ : Nontrivial R
⊢ ∀ (n : ℕ) (c : R), c ≠ 0 → natDegree (↑(taylor r) (↑(monomial n) c)) = n
intro n c c0
no goals
R : Type u_1
inst✝ : Semiring R
r✝ : R
f p : R[X]
r : R
✝ : Nontrivial R
n : ℕ
c : R
c0 : c ≠ 0
⊢ natDegree (↑(taylor r) (↑(monomial n) c)) = n
simp [taylor_monomial, natDegree_C_mul_eq_of_mul_ne_zero, natDegree_pow_X_add_C, c0]