instSMulMemClass

Mathlib.Topology.Algebra.Module.ClosedSubmodule

URI: https://scilib.ai/kg/mathlib#ClosedSubmodule.instSMulMemClass

English

ClosedSubmodule R M is a SMulMemClass, i.e., closed under scalar multiplication by elements of R.

Русский

ClosedSubmodule R M образует SMulMemClass, то есть замкнуто относительно умножения скалярами из R.

LaTeX

$$$\text{ClosedSubmodule}(R,M)\text{ is SMulMemClass }(R,M).$$$

Lean4

instance : SMulMemClass (ClosedSubmodule R M) R M where smul_mem {s} r := s.smul_mem r

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

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

Разделы

Аффилиация

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