smulMemClass

Mathlib.Algebra.Module.Submodule.Defs

URI: https://scilib.ai/kg/mathlib#Submodule.smulMemClass

English

Submodule R M is endowed with an SMulMemClass, i.e., scalar multiplication preserves the submodule.

Русский

Подмодуль Submodule R M обладает SMulMemClass, т.е. умножение на скаляры сохраняет подмодуль.

LaTeX

$$$\\operatorname{SMulMemClass} (\\text{Submodule } R M) R M$$$

Lean4

instance smulMemClass : SMulMemClass (Submodule R M) R M where
  smul_mem {s} c _ h := SubMulAction.smul_mem' s.toSubMulAction c h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru