instIsTwoSidedTop

Mathlib.RingTheory.Ideal.Lattice

URI: https://scilib.ai/kg/mathlib#Ideal.instIsTwoSidedTop

English

In any semiring α, the top ideal ⊤ is a two-sided ideal.

Русский

В любом полугруппе-кольце α верхний идеал ⊤ является двусторонним идеалом.

LaTeX

$$$IsTwoSided(\\\\top : \\\\mathrm{Ideal}\\\\,\\\\alpha)$$$

Lean4

instance (priority := low) : IsTwoSided (⊤ : Ideal α) :=
  ⟨fun _ _ ↦ trivial⟩

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

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

Разделы

Аффилиация

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