instZero_1

Mathlib.Algebra.Lie.Submodule

URI: https://scilib.ai/kg/mathlib#LieSubmodule.instZero_1

English

There is a zero LieSubmodule defined as the bottom element.

Русский

Существует нулевой Ли-подмодуль, равный нижнему элементу.

LaTeX

$$$\text{Zero }(\text{LieSubmodule } R\ L\ M) :\;= \;\bot$$$

Lean4

instance : Zero (LieSubmodule R L M) where zero := ⊥

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

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

Разделы

Аффилиация

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