Theorems · Theorem · linear algebra

Lagrange.nodal_insert_eq_nodal

∀ {R : Type u_1} [inst : CommRing R] {ι : Type u_2} {s : Finset ι} {v : ι → R} [inst_1 : DecidableEq ι] {i : ι},
  i ∉ s → Lagrange.nodal (insert i s) v = (Polynomial.X - Polynomial.C (v i)) * Lagrange.nodal s v

Defined in

Mathlib.LinearAlgebra.Lagrange

Cited by

1 results in Mathlib

Foundations

Depth 102 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingDecidableEq