Theorems · Definition · ring theory
SkewPolynomial.support
{R : Type u_1} → [inst : Semiring R] → SkewPolynomial R → Finset ℕThe set of all n such that X^n has a non-zero coefficient.
- Defined in
- Mathlib.Algebra.SkewPolynomial.Basic
- Cited by
- 30 results in Mathlib
- Foundations
- Depth 27 from the axioms · uses propext, 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.
- DFunLike.coeproof · cited by 62,936
- Semiringstatement and proof · cited by 13,802
- Finsetstatement · cited by 13,712
- Finset.mapproof · cited by 747
- Multiplicative.toAddproof · cited by 161
- SkewPolynomialstatement and proof · cited by 124
- SkewMonoidAlgebra.supportproof · cited by 45
Cited by30
Results whose statement or proof uses this declaration.
- SkewPolynomial.support_eq_skewMonoidAlgebra_supportstatement · cited by 5
- SkewPolynomial.support_monomialstatement · cited by 4
- SkewPolynomial.sum_defstatement and proof · cited by 3
- SkewPolynomial.support_monomial_subsetstatement · cited by 3
- SkewPolynomial.support_C_mul_X_pow_subsetstatement and proof · cited by 2
- SkewPolynomial.support_addstatement · cited by 2
- SkewPolynomial.support_updatestatement · cited by 1
- SkewPolynomial.support_zerostatement · cited by 1
- SkewPolynomial.sum_add'proof · cited by 1
- SkewPolynomial.sum_negproof · cited by 1
- SkewPolynomial.support_X_powstatement and proof · cited by 1
- SkewPolynomial.support_erasestatement · cited by 1