rootMultiplicity_X_sub_C_self — Mathlib

English

Root multiplicity remains invariant under certain polynomial transformations (simplicial in the formal statement).

Русский

Кратность корня сохраняется под определёнными преобразованиями многочлена.

LaTeX

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

Lean4

theorem rootMultiplicity_X_sub_C_self [Nontrivial R] {x : R} : rootMultiplicity x (X - C x) = 1 :=
  pow_one (X - C x) ▸ rootMultiplicity_X_sub_C_pow x 1

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