Theorems · Definition · ring theory
SkewPolynomial.coeff
{R : Type u_1} → [inst : Semiring R] → SkewPolynomial R → ℕ → Rcoeff p n is the coefficient of X ^ n in p.
- Defined in
- Mathlib.Algebra.SkewPolynomial.Basic
- Cited by
- 37 results in Mathlib
- Foundations
- Depth 59 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.
Cites5
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
- Multiplicative.ofAddproof · cited by 237
- SkewPolynomialstatement and proof · cited by 124
- SkewMonoidAlgebra.coeffproof · cited by 110
Cited by37
Results whose statement or proof uses this declaration.
- SkewPolynomial.coeff_monomialstatement · cited by 8
- SkewPolynomial.coeff_Cstatement and proof · cited by 3
- SkewPolynomial.coeff_erasestatement · cited by 3
- SkewPolynomial.sum_defstatement and proof · cited by 3
- SkewPolynomial.coeff_natCast_itestatement and proof · cited by 2
- SkewPolynomial.coeff_update_applystatement · cited by 2
- SkewPolynomial.update_zero_eq_eraseproof · cited by 1
- SkewPolynomial.coeff_C_zerostatement · cited by 1
- SkewPolynomial.coeff_Xstatement · cited by 1
- SkewPolynomial.coeff_X_onestatement · cited by 1
- SkewPolynomial.coeff_addstatement · cited by 1
- SkewPolynomial.coeff_updatestatement and proof · cited by 1