sum — Mathlib

English

The finite sum of polynomials, each homogeneous of degree n, is homogeneous of degree n.

Русский

Конечная сумма полиномов, каждый из которых однороден степени n, является однородной степени n.

LaTeX

$$For Finite set s and φ_i, if ∀ i ∈ s, IsHomogeneous(φ_i, n), then IsHomogeneous(∑ i ∈ s, φ_i, n).$$

Lean4

theorem sum {ι : Type*} (s : Finset ι) (φ : ι → MvPolynomial σ R) (n : ℕ) (h : ∀ i ∈ s, IsHomogeneous (φ i) n) :
    IsHomogeneous (∑ i ∈ s, φ i) n :=
  (homogeneousSubmodule σ R n).sum_mem h

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