Theorems · Theorem · commutative algebra

MvPolynomial.IsWeightedHomogeneous.add

∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M]
  {φ ψ : MvPolynomial σ R} {n : M} {w : σ → M},
  MvPolynomial.IsWeightedHomogeneous w φ n →
    MvPolynomial.IsWeightedHomogeneous w ψ n → MvPolynomial.IsWeightedHomogeneous w (φ + ψ) n

The sum of two weighted homogeneous polynomials of degree n is weighted homogeneous of weighted degree n.

Defined in: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Cited by: 2 results in Mathlib
Foundations: Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommSemiring AddCommMonoid

Mathlib docs Source Loogle LeanSearch

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.

AddCommMonoidstatement and proof · cited by 12,281
CommSemiringstatement and proof · cited by 10,911
Finsuppstatement · cited by 5,255
MvPolynomialstatement and proof · cited by 2,140
Submodule.add_memproof · cited by 75
MvPolynomial.IsWeightedHomogeneousstatement and proof · cited by 31
MvPolynomial.weightedHomogeneousSubmoduleproof · cited by 23

Cited by2

Results whose statement or proof uses this declaration.

MvPolynomial.IsWeightedHomogeneous.induction_onstatement and proof · cited by 1
MvPolynomial.IsWeightedHomogeneous.pderivproof · cited by 1