mem_weightedHomogeneousSubmodule — Mathlib

English

An element p belongs to weightedHomogeneousSubmodule R w m if and only if p is weighted homogeneous of degree m.

Русский

Элемент p принадлежит weightedHomogeneousSubmodule R w m тогда и только тогда, когда p взвешенно однороден степени m.

LaTeX

$$$p \\in weightedHomogeneousSubmodule\\,R\\,w\\,m \\;\\Longleftrightarrow\\; p\\ IsWeightedHomogeneous\\ w\\ p\\ m$$

Lean4

@[simp]
theorem mem_weightedHomogeneousSubmodule (w : σ → M) (m : M) (p : MvPolynomial σ R) :
    p ∈ weightedHomogeneousSubmodule R w m ↔ p.IsWeightedHomogeneous w m :=
  Iff.rfl

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