Theorems · Theorem · field theory

Polynomial.eval_iterate_derivative_rootMultiplicity

∀ {R : Type u} [inst : CommRing R] {p : Polynomial R} {t : R},
  Polynomial.eval t ((⇑Polynomial.derivative)^[Polynomial.rootMultiplicity t p] p) =
    (Polynomial.rootMultiplicity t p).factorial •
      Polynomial.eval t (p /ₘ (Polynomial.X - Polynomial.C t) ^ Polynomial.rootMultiplicity t p)

Defined in

Mathlib.Algebra.Polynomial.FieldDivision

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRing