instCompleteLattice

Mathlib.RingTheory.TwoSidedIdeal.Lattice

URI: https://scilib.ai/kg/mathlib#TwoSidedIdeal.instCompleteLattice

Lean4

instance : CompleteLattice (TwoSidedIdeal R)
    where
  __ := (inferInstance : SemilatticeSup (TwoSidedIdeal R))
  __ := (inferInstance : SemilatticeInf (TwoSidedIdeal R))
  __ := (inferInstance : CompleteSemilatticeSup (TwoSidedIdeal R))
  __ := (inferInstance : CompleteSemilatticeInf (TwoSidedIdeal R))
  le_top _ := by rw [ringCon_le_iff]; exact le_top
  bot_le _ := by rw [ringCon_le_iff]; exact bot_le

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

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

Разделы

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

Аффилиация

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