Theorems · Theorem · linear algebra
Lagrange.nodal_eq_mul_nodal_erase
∀ {R : Type u_1} [inst : CommRing R] {ι : Type u_2} {s : Finset ι} {v : ι → R} [inst_1 : DecidableEq ι] {i : ι},
i ∈ s → Lagrange.nodal s v = (Polynomial.X - Polynomial.C (v i)) * Lagrange.nodal (s.erase i) v- Defined in
- Mathlib.LinearAlgebra.Lagrange
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 102 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommRingDecidableEq
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- CommRingstatement and proof · cited by 17,173
- Finsetstatement and proof · cited by 13,712
- RingHomstatement · cited by 10,189
- Polynomialstatement · cited by 5,681
- Finset.prodproof · cited by 2,356
- Polynomial.Xstatement and proof · cited by 1,639
- Polynomial.Cstatement and proof · cited by 1,598
- Finset.erasestatement · cited by 455
- Lagrange.nodalstatement · cited by 24
- Finset.mul_prod_eraseproof · cited by 23
Cited by2
Results whose statement or proof uses this declaration.
- Lagrange.nodal_erase_eq_nodal_divproof · cited by 2
- Lagrange.X_sub_C_dvd_nodalproof · cited by 0