instOrderTop

Mathlib.Algebra.Module.Submodule.Lattice

URI: https://scilib.ai/kg/mathlib#Submodule.instOrderTop

English

The submodule lattice is equipped with an order where ⊤ is the greatest element.

Русский

Решетка подмодулей оснащена порядком, в котором ⊤ — наибольший элемент.

LaTeX

$$$\text{For all } p, p \le \top$$$

Lean4

instance : OrderTop (Submodule R M) where
  top := ⊤
  le_top _ _ _ := trivial

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

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

Разделы

Аффилиация

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