mem_homogeneousSubmodule — Mathlib

English

The homogeneous submodule of degree n equals the finsupp-supported set of monomials of degree n.

Русский

Однородный подмодуль степени n равен подмножеству, поддерживаемому FinSupp из мономов степени n.

LaTeX

$$$\\text{homogeneousSubmodule}(\\sigma,R,n) = \\mathrm{Finsupp.supported}_{R} \\{ d : \\sigma \\to \\mathbb{N} \\mid d.degree = n \\}$$$

Lean4

@[simp]
theorem mem_homogeneousSubmodule (n : ℕ) (p : MvPolynomial σ R) : p ∈ homogeneousSubmodule σ R n ↔ p.IsHomogeneous n :=
  Iff.rfl

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