orderBot

Mathlib.RingTheory.FractionalIdeal.Basic

URI: https://scilib.ai/kg/mathlib#FractionalIdeal.orderBot

English

The bottom element of FractionalIdeal equals the zero fractional ideal.

Русский

Нижний элемент FractionalIdeal равен нулевому дробному идеалу.

LaTeX

$$$\bot = 0$$$

Lean4

instance orderBot : OrderBot (FractionalIdeal S P) where
  bot := 0
  bot_le := zero_le

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

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

Разделы

Аффилиация

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