Theorems · Definition · commutative algebra
Polynomial.degreeLT
(R : Type u) → [inst : Semiring R] → ℕ → Submodule R (Polynomial R)
The R-submodule of R[X] consisting of polynomials of degree < n.
- Defined in
- Mathlib.RingTheory.Polynomial.Basic
- Cited by
- 47 results in Mathlib
- Foundations
- Depth 96 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.
Cites6
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
- iInfproof · cited by 1,690
- LinearMap.kerproof · cited by 848
- Polynomial.lcoeffproof · cited by 11
Cited by56
Results whose statement or proof uses this declaration.
- Polynomial.degreeLT.basisstatement · cited by 15
- Polynomial.mem_degreeLTstatement · cited by 14
- Polynomial.degreeLT.addLinearEquivstatement · cited by 12
- Polynomial.sylvesterMapstatement and proof · cited by 7
- Polynomial.degreeLT.basis_valstatement · cited by 4
- Polynomial.taylorLinearEquivstatement and proof · cited by 4
- Polynomial.degreeLTEquivstatement and proof · cited by 4
- Polynomial.degreeLT.basisProdstatement · cited by 4
- Polynomial.monicEquivDegreeLTstatement and proof · cited by 3
- Polynomial.sylvesterMap_apply_coestatement and proof · cited by 3
- Polynomial.adjSylvesterstatement · cited by 3
- Matrix.charpoly_sub_diagonal_degree_ltproof · cited by 3