Theorems · Theorem · linear algebra
Lagrange.eval_basis_self
∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {s : Finset ι} {v : ι → F} {i : ι},
Set.InjOn v ↑s → i ∈ s → Polynomial.eval (v i) (Lagrange.basis s v i) = 1- Defined in
- Mathlib.LinearAlgebra.Lagrange
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 108 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- FieldDecidableEq
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement and proof · cited by 13,712
- SetLike.coestatement and proof · cited by 8,199
- Fieldstatement and proof · cited by 7,404
- Polynomialproof · cited by 5,681
- Polynomial.evalstatement and proof · cited by 796
- Set.InjOnstatement and proof · cited by 543
- Finset.eraseproof · cited by 455
- Finset.mem_eraseproof · cited by 61
- Lagrange.basisstatement · cited by 26
- Finset.prod_eq_oneproof · cited by 22
- Lagrange.basisDivisorproof · cited by 19
- Polynomial.eval_prodproof · cited by 15
Cited by3
Results whose statement or proof uses this declaration.
- Lagrange.eval_interpolate_at_nodeproof · cited by 5
- Lagrange.sum_basisproof · cited by 3
- Lagrange.interpolate_eq_sum_interpolate_insert_sdiffproof · cited by 1