Theorems · Definition · ring theory
SkewPolynomial.monomial
{R : Type u_1} → ℕ → [inst : Semiring R] → R →ₗ[R] SkewPolynomial Rmonomial s a is the monomial a * X ^ s.
- Defined in
- Mathlib.Algebra.SkewPolynomial.Basic
- Cited by
- 49 results in Mathlib
- Foundations
- Depth 75 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.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- RingHom.idstatement · cited by 18,349
- Semiringstatement and proof · cited by 13,802
- LinearMapstatement · cited by 10,215
- Multiplicativestatement · cited by 875
- Multiplicative.ofAddproof · cited by 237
- SkewPolynomialstatement · cited by 124
- SkewMonoidAlgebra.lsingleproof · cited by 4
Cited by50
Results whose statement or proof uses this declaration.
- SkewPolynomial.Xproof · cited by 27
- SkewPolynomial.coeff_monomialstatement · cited by 8
- SkewPolynomial.monomial_mul_monomialstatement and proof · cited by 5
- SkewPolynomial.sum_monomial_indexstatement · cited by 5
- SkewPolynomial.support_monomialstatement · cited by 4
- SkewPolynomial.C_mul_X_pow_eq_monomialstatement · cited by 3
- SkewPolynomial.coeff_Cproof · cited by 3
- SkewPolynomial.support_monomial_subsetstatement · cited by 3
- SkewPolynomial.C_mul_X_eq_monomialstatement · cited by 2
- SkewPolynomial.X_mulstatement and proof · cited by 2
- SkewPolynomial.X_pow_eq_monomialstatement and proof · cited by 2
- SkewPolynomial.monomial_addstatement · cited by 2