Theorems · Theorem · field theory

Polynomial.eval_divByMonic_eq_trailingCoeff_comp

∀ {R : Type u} [inst : CommRing R] {p : Polynomial R} {t : R},
  Polynomial.eval t (p /ₘ (Polynomial.X - Polynomial.C t) ^ Polynomial.rootMultiplicity t p) =
    (p.comp (Polynomial.X + Polynomial.C t)).trailingCoeff

Defined in

Mathlib.Algebra.Polynomial.Div

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRing