subProdXSubC — Mathlib

English

For a monic polynomial f, subProdXSubC(f) equals f minus the product over its roots of (X − X_{f,i}).

Русский

Для монического многочлена f полином subProdXSubC(f) равен f минус произведение по корням (X − X_{f,i}).

LaTeX

$$$\\mathrm{subProdXSubC}(f) = f.1.map(\\mathrm{algebraMap}\\; _ _) - \\prod_{i=Fin f.1.natDegree} (X - C(\\mathrm{MvPolynomial}.X \\langle f, i \\rangle))$$$

Lean4

/-- Given a monic polynomial `f : k[X]`,
`subProdXSubC f` is the polynomial $f - \prod_i (X - X_{f,i})$. -/
def subProdXSubC (f : Monics k) : (MvPolynomial (Vars k) k)[X] :=
  f.1.map (algebraMap _ _) - ∏ i : Fin f.1.natDegree, (X - C (MvPolynomial.X ⟨f, i⟩))

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