instZero

Mathlib.Algebra.Lie.Submodule

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

← MathLib Explorer

English

The zero module is a Lie submodule of any Lie module.

Русский

Нулевой модуль является подмодулем Ли любого модуля Ли.

LaTeX

$$$0 \\text{ is a LieSubmodule of } M$$$

Lean4

/-- The zero module is a Lie submodule of any Lie module. -/
instance : Zero (LieSubmodule R L M) :=
  ⟨{ (0 : Submodule R M) with lie_mem := fun {x m} h ↦ by rw [(Submodule.mem_bot R).1 h]; apply lie_zero }⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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