Theorems · Theorem · commutative algebra
Polynomial.mem_degreeLT
∀ {R : Type u} [inst : Semiring R] {n : ℕ} {f : Polynomial R}, f ∈ Polynomial.degreeLT R n ↔ f.degree < ↑n- Defined in
- Mathlib.RingTheory.Polynomial.Basic
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 97 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.
Cites11
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 and proof · cited by 5,681
- iInfproof · cited by 1,690
- WithBotstatement · cited by 1,498
- LinearMap.kerproof · cited by 848
- Polynomial.degreestatement and proof · cited by 643
- iInf_congr_Propproof · cited by 218
- Polynomial.degreeLTstatement · cited by 47
- Polynomial.lcoeffproof · cited by 11
- Polynomial.degree_lt_iff_coeff_zeroproof · cited by 5
Cited by14
Results whose statement or proof uses this declaration.
- Polynomial.Sequence.span_degreeLTproof · cited by 3
- Matrix.charpoly_sub_diagonal_degree_ltproof · cited by 3
- Polynomial.eq_of_degrees_lt_of_eval_index_eqproof · cited by 2
- Polynomial.degreeLT.addLinearEquiv_apply'proof · cited by 2
- Polynomial.eq_zero_of_degree_lt_of_eval_finset_eq_zeroproof · cited by 2
- Polynomial.eq_of_degrees_lt_of_eval_finset_eqproof · cited by 1
- Polynomial.eval_eq_sum_degreeLTEquivproof · cited by 1
- Polynomial.degreeLT_succ_eq_degreeLEproof · cited by 1
- Polynomial.exists_degree_le_of_mem_spanproof · cited by 1
- Polynomial.monomial_coe_mem_degreeLTproof · cited by 0
- Polynomial.Chebyshev.integral_eq_sumZeroesproof · cited by 0
- Polynomial.degreeLT_eq_span_X_powproof · cited by 0