rootMultiplicity_eq_natTrailingDegree

English

Multiplicity at t equals the natTrailingDegree of p ∘ (X + C t).

Русский

Кратность корня t равна natTrailingDegree от p ∘ (X + C t).

LaTeX

$$$$ \\operatorname{rootMultiplicity} t\, p = \\operatorname{natTrailingDegree}\\big(p \\circ (X + C t)\\big). $$$$

Lean4

/-- See `Polynomial.rootMultiplicity_eq_natTrailingDegree'` for the special case of `t = 0`. -/
theorem rootMultiplicity_eq_natTrailingDegree {p : R[X]} {t : R} :
    p.rootMultiplicity t = (p.comp (X + C t)).natTrailingDegree :=
  rootMultiplicity_eq_rootMultiplicity.trans rootMultiplicity_eq_natTrailingDegree'

Похожие утверждения