instAddSubmonoidClassHomogeneousSubmodule

English

The collection of homogeneous submodules forms an additive submonoid class, with zero and addition closed.

Русский

Множество однородных подмодулей образует класс подмножества с нулём и операцией сложения, замкнутое под суммированием.

LaTeX

$$$$ \text{AddSubmonoidClass } (\text{HomogeneousSubmodule } 𝒜 \ℳ) \; M. $$$$

Lean4

instance : AddSubmonoidClass (HomogeneousSubmodule 𝒜 ℳ) M
    where
  zero_mem p := p.toSubmodule.zero_mem
  add_mem hx hy := Submodule.add_mem _ hx hy

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