Theorems · Theorem · commutative algebra
MvPolynomial.notMem_support_iff
∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p : MvPolynomial σ R} {m : σ →₀ ℕ},
m ∉ p.support ↔ MvPolynomial.coeff m p = 0- Defined in
- Mathlib.Algebra.MvPolynomial.Basic
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 63 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommSemiring
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.
- Finsetstatement · cited by 13,712
- CommSemiringstatement and proof · cited by 10,911
- Finsuppstatement and proof · cited by 5,255
- MvPolynomialstatement and proof · cited by 2,140
- MvPolynomial.coeffstatement and proof · cited by 315
- MvPolynomial.supportstatement · cited by 220
Cited by12
Results whose statement or proof uses this declaration.
- MvPolynomial.C_dvd_iff_dvd_coeffproof · cited by 3
- MvPolynomial.coeff_rename_eq_zeroproof · cited by 3
- MvPolynomial.coeff_toPolynomialAdjoinImageCompl_ne_zeroproof · cited by 2
- MvPolynomial.coeffs_addproof · cited by 2
- MvPolynomial.disjoint_support_monomialproof · cited by 2
- MvPolynomial.X_dvd_mul_iffproof · cited by 1
- MvPolynomial.notMem_support_sub_monomial_sub_monomialproof · cited by 1
- MvPolynomial.eval₂_memproof · cited by 1
- MonomialOrder.sPolynomial_decompositionproof · cited by 1
- MvPolynomial.eq_divMonomial_singleproof · cited by 1
- MvPolynomial.eq_modMonomial_single_iffproof · cited by 1
- MvPolynomial.eq_monomial_of_support_subset_singletonproof · cited by 1