instIsModularLattice

Mathlib.Algebra.Lie.Submodule

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

← MathLib Explorer

English

The lattice of Lie submodules is modular.

Русский

Решётка подмодулей Ли модульна.

LaTeX

$$IsModularLattice (LieSubmodule R L M)$$

Lean4

instance : IsModularLattice (LieSubmodule R L M) where
  sup_inf_le_assoc_of_le _
    _ := by
    simp only [← toSubmodule_le_toSubmodule, sup_toSubmodule, inf_toSubmodule]
    exact IsModularLattice.sup_inf_le_assoc_of_le _

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

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

Разделы

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

Аффилиация

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