sum — Mathlib

English

The sum over a finite set of weighted homogeneous polynomials of degree n is weighted homogeneous of degree n.

Русский

Сумма по конечному индексу взвешенно однородных по степени n полиномов сохраняет степень n.

LaTeX

$$s.sum (fun i => φ i) has degree n if each φ i has degree n$$

Lean4

/-- The sum of weighted homogeneous polynomials of degree `n` is weighted homogeneous of
  weighted degree `n`. -/
theorem sum {ι : Type*} (s : Finset ι) (φ : ι → MvPolynomial σ R) (n : M) {w : σ → M}
    (h : ∀ i ∈ s, IsWeightedHomogeneous w (φ i) n) : IsWeightedHomogeneous w (∑ i ∈ s, φ i) n :=
  (weightedHomogeneousSubmodule R w n).sum_mem h

Похожие утверждения