instZeroLieSubalgebra

Mathlib.Algebra.Lie.Subalgebra

URI: https://scilib.ai/kg/mathlib#instZeroLieSubalgebra

Lean4

/-- The zero algebra is a subalgebra of any Lie algebra. -/
instance : Zero (LieSubalgebra R L) :=
  ⟨⟨0,
      @fun x y hx _hy ↦ by
        rw [(Submodule.mem_bot R).1 hx, zero_lie]
        exact Submodule.zero_mem 0⟩⟩

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

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

Разделы

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

Аффилиация

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