instAddSubgroupClass — Mathlib

English

LieSubmodule is closed under scalar multiplication: for any N and a in R, and m in N, a·m ∈ N.

Русский

Подмодуль Ли замкнут относительно умножения на скаляр: для любого N, a в R и m в N, a·m ∈ N.

LaTeX

$$$\\forall N\\ (\\forall a\\in R)(\\forall m\\in N), a\\cdot m\\in N$$$

Lean4

instance : AddSubgroupClass (LieSubmodule R L M) M
    where
  add_mem {N} _ _ := N.add_mem'
  zero_mem N := N.zero_mem'
  neg_mem {N} x hx := show -x ∈ N.toSubmodule from neg_mem hx

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