Theorems · Theorem · field theory

Polynomial.coeff_divByMonic_X_sub_C

∀ {R : Type u} [inst : Ring R] (p : Polynomial R) (a : R) (n : ℕ),
  (p /ₘ (Polynomial.X - Polynomial.C a)).coeff n = ∑ i ∈ Finset.Icc (n + 1) p.natDegree, a ^ (i - (n + 1)) * p.coeff i

Defined in

Mathlib.Algebra.Polynomial.Div

Cited by

0 results in Mathlib

Foundations

Depth 123 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Ring