Theorems · Definition · commutative algebra
Polynomial.degreeLT.basis
(R : Type u_1) → [inst : Semiring R] → (n : ℕ) → Module.Basis (Fin n) R ↥(Polynomial.degreeLT R n)
Basis for R[X]_n given by X^i with i < n.
- Defined in
- Mathlib.RingTheory.Polynomial.DegreeLT
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 105 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Semiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Semiringstatement and proof · cited by 13,802
- Submodulestatement · cited by 7,192
- Polynomialstatement · cited by 5,681
- Module.Basisstatement · cited by 1,477
- Polynomial.degreeLTstatement · cited by 47
- Module.Basis.ofEquivFunproof · cited by 7
- Polynomial.degreeLTEquivproof · cited by 4
Cited by18
Results whose statement or proof uses this declaration.
- Polynomial.degreeLT.addLinearEquivproof · cited by 12
- Polynomial.degreeLT.basis_valstatement · cited by 4
- Polynomial.degreeLT.basisProdproof · cited by 4
- Polynomial.adjSylvesterproof · cited by 3
- Polynomial.toMatrix_sylvesterMap'statement and proof · cited by 2
- Polynomial.sylveserMap_comp_adjSylvesterproof · cited by 1
- Polynomial.degreeLT.basis_reprstatement · cited by 1
- Polynomial.det_taylorLinearEquiv_toLinearMapproof · cited by 1
- Polynomial.degreeLT.addLinearEquiv_castAddstatement and proof · cited by 1
- Polynomial.degreeLT.addLinearEquiv_natAddstatement and proof · cited by 1
- Polynomial.degreeLT.addLinearEquiv_symm_apply_inlproof · cited by 1
- Polynomial.degreeLT.addLinearEquiv_symm_apply_inl_basisstatement · cited by 1