nodal_eq_mul_nodal_erase — Mathlib

English

Nodal polynomials factor by removing a node, multiplied by a linear factor.

Русский

Если i ∈ s, то nodal(s,v) = (X − v(i)) · nodal(s\\{i}, v).

LaTeX

$$$ \\operatorname{nodal}(s,v,i) = (X - C(v(i))) \\cdot \\operatorname{nodal}(s\\setminus i,v). $$$

Lean4

theorem nodal_eq_mul_nodal_erase [DecidableEq ι] {i : ι} (hi : i ∈ s) :
    nodal s v = (X - C (v i)) * nodal (s.erase i) v := by
  simp_rw [nodal, Finset.mul_prod_erase _ (fun x => X - C (v x)) hi]

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