Theorems · Theorem · linear algebra
Lagrange.natDegree_basis
∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {s : Finset ι} {v : ι → F} {i : ι},
Set.InjOn v ↑s → i ∈ s → (Lagrange.basis s v i).natDegree = s.card - 1- Defined in
- Mathlib.LinearAlgebra.Lagrange
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 114 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.
Cites17
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
- Finset.sumproof · cited by 5,195
- Finset.prodproof · cited by 2,356
- Finset.cardstatement · cited by 2,327
- Finset.sum_congrproof · cited by 2,323
- Polynomial.natDegreestatement and proof · cited by 1,105
- Set.InjOnstatement and proof · cited by 543
- Finset.eraseproof · cited by 455
- Finset.card_erase_of_memproof · cited by 38
- Lagrange.basisstatement and proof · cited by 26
Cited by3
Results whose statement or proof uses this declaration.
- Lagrange.degree_basisproof · cited by 3
- Lagrange.leadingCoeff_basisproof · cited by 1
- Lagrange.coeff_eq_sumproof · cited by 1