Theorems · Theorem · commutative algebra

MvPolynomial.weightedHomogeneousComponent_C_mul

∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] {w : σ → M}
  (φ : MvPolynomial σ R) (n : M) (r : R),
  (MvPolynomial.weightedHomogeneousComponent w n) (MvPolynomial.C r * φ) =
    MvPolynomial.C r * (MvPolynomial.weightedHomogeneousComponent w n) φ

Defined in

Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Cited by

1 results in Mathlib

Foundations

Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringAddCommMonoid