X_sub_C_mul_removeFactor — Mathlib

English

In the extension by a root, the product (X - root) times removeFactor equals the mapped original polynomial.

Русский

В расширении по корню произведение (X − корень) на removeFactor равно отображенному исходному многочлену.

LaTeX

$$$\\bigl(X - C(\\text{AdjoinRoot.root }f.{\\text{factor}})\\bigr) \\cdot f.removeFactor = \\text{map}(\\text{AdjoinRoot.of }f.{\\text{factor}})\\,f$$$

Lean4

theorem X_sub_C_mul_removeFactor (f : K[X]) (hf : f.natDegree ≠ 0) :
    (X - C (AdjoinRoot.root f.factor)) * f.removeFactor = map (AdjoinRoot.of f.factor) f :=
  by
  let ⟨g, hg⟩ := factor_dvd_of_natDegree_ne_zero hf
  apply (mul_divByMonic_eq_iff_isRoot (R := AdjoinRoot f.factor) (a := AdjoinRoot.root f.factor)).mpr
  rw [IsRoot.def, eval_map, hg, eval₂_mul, ← hg, AdjoinRoot.eval₂_root, zero_mul]

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