mul — Mathlib

English

The product of weighted homogeneous polynomials of degrees m and n is weighted homogeneous of degree m+n.

Русский

Произведение взвешенно однородных полиномов степеней m и n — взвешенно однородно степени m+n.

LaTeX

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

Lean4

/-- The product of weighted homogeneous polynomials of weighted degrees `m` and `n` is weighted
  homogeneous of weighted degree `m + n`. -/
theorem mul {w : σ → M} (hφ : IsWeightedHomogeneous w φ m) (hψ : IsWeightedHomogeneous w ψ n) :
    IsWeightedHomogeneous w (φ * ψ) (m + n) :=
  weightedHomogeneousSubmodule_mul w m n <| Submodule.mul_mem_mul hφ hψ

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