Theorems · Theorem · field theory
Polynomial.smul_C
∀ {R : Type u} [inst : Semiring R] {S : Type u_1} [inst_1 : SMulZeroClass S R] (s : S) (r : R),
s • Polynomial.C r = Polynomial.C (s • r)- Defined in
- Mathlib.Algebra.Polynomial.Basic
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 101 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- SemiringSMulZeroClass
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.coestatement · cited by 62,936
- Semiringstatement and proof · cited by 13,802
- RingHomstatement · cited by 10,189
- Polynomialstatement · cited by 5,681
- Polynomial.Cstatement · cited by 1,598
- SMulZeroClassstatement and proof · cited by 213
- Polynomial.smul_monomialproof · cited by 5
Cited by9
Results whose statement or proof uses this declaration.
- Polynomial.smul_eval_smulproof · cited by 2
- FixedPoints.smul_polynomialproof · cited by 1
- prodXSubSMul.smulproof · cited by 1
- MulSemiringAction.charpoly_eq_prod_smulproof · cited by 1
- Polynomial.iterate_derivative_eq_factorial_smul_sumproof · cited by 1
- Polynomial.nnqsmul_eq_C_mulproof · cited by 0
- Polynomial.qsmul_eq_C_mulproof · cited by 0
- AdjoinRoot.smul_ofproof · cited by 0
- Polynomial.bernoulli_oneproof · cited by 0