instIsTwoSidedBot

Mathlib.RingTheory.Ideal.Lattice

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

English

In any semiring α, the bottom ideal ⊥ is a two-sided ideal.

Русский

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

LaTeX

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

Lean4

instance (priority := low) : IsTwoSided (⊥ : Ideal α) :=
  ⟨fun _ h ↦ by rw [h, zero_mul]; exact zero_mem _⟩

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

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

Разделы

Аффилиация

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