Theorems · Theorem · commutative algebra

MvPolynomial.weightedHomogeneousComponent_directSum

∀ (R : Type u_1) {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] (w : σ → M)
  [inst_2 : DecidableEq M] (x : DirectSum M fun i => ↥(MvPolynomial.weightedHomogeneousSubmodule R w i)) (m : M),
  (MvPolynomial.weightedHomogeneousComponent w m)
      ((DirectSum.coeLinearMap fun i => MvPolynomial.weightedHomogeneousSubmodule R w i) x) =
    ↑(x m)

Defined in

Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidDecidableEq