R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n✝ : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
n : ℕ
hn : degree q ≤ ↑n
✝ : Nontrivial R
⊢ ∑ i : Fin n, ↑(monomial ↑i) (coeff (p %ₘ q) ↑i) = p %ₘ q
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n✝ : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
n : ℕ
hn : degree q ≤ ↑n
⊢ ∑ i : Fin n, ↑(monomial ↑i) (coeff (p %ₘ q) ↑i) = p %ₘ q
nontriviality R
no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n✝ : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
n : ℕ
hn : degree q ≤ ↑n
✝ : Nontrivial R
⊢ ∑ i : Fin n, ↑(monomial ↑i) (coeff (p %ₘ q) ↑i) = p %ₘ q
exact
  (sum_fin (fun i c => monomial i c) (by simp) ((degree_modByMonic_lt _ hq).trans_le hn)).trans
    (sum_monomial_eq _)
no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n✝ : ℕ
inst✝ : CommRing R
p q : R[X]
hq : Monic q
n : ℕ
hn : degree q ≤ ↑n
✝ : Nontrivial R
⊢ ∀ (i : ℕ), (fun i c => ↑(monomial i) c) i 0 = 0
simp