instOrderBot

Mathlib.Algebra.Module.Submodule.Lattice

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

English

The bottom element defines the minimal submodule in the order of inclusion: ⊥ ≤ p for every submodule p.

Русский

Нижний элемент задаёт минимальный подмодуль в порядке включения: ⊥ ⊆ p для любого подмодуля p.

LaTeX

$$⊥ ≤ p for all p$$

Lean4

instance : OrderBot (Submodule R M) where
  bot := ⊥
  bot_le p x := by simp +contextual [zero_mem]

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

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

Разделы

Аффилиация

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