homogeneousSubmodule_mul — Mathlib

English

If a degree vector d has degree n, then the monomial d mapped with coefficient r is homogeneous of degree n.

Русский

Если вектор степени d имеет степень n, то моном d с коэффициентом r однороден степени n.

LaTeX

$$$\\text{IsHomogeneous}(\\mathrm{monomial}(d,r),n)$ whenever $d.degree = n$$$

Lean4

theorem homogeneousSubmodule_mul (m n : ℕ) :
    homogeneousSubmodule σ R m * homogeneousSubmodule σ R n ≤ homogeneousSubmodule σ R (m + n) :=
  weightedHomogeneousSubmodule_mul 1 m n

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