add — Mathlib

English

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

Русский

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

LaTeX

$$IsWeightedHomogeneous w φ n → IsWeightedHomogeneous w ψ n → IsWeightedHomogeneous w (φ+ψ) n$$

Lean4

/-- The sum of two weighted homogeneous polynomials of degree `n` is weighted homogeneous of
  weighted degree `n`. -/
theorem add {w : σ → M} (hφ : IsWeightedHomogeneous w φ n) (hψ : IsWeightedHomogeneous w ψ n) :
    IsWeightedHomogeneous w (φ + ψ) n :=
  (weightedHomogeneousSubmodule R w n).add_mem hφ hψ

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