instMax

Mathlib.RingTheory.FractionalIdeal.Basic

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

English

The maximum of two fractional ideals is their sum, and it is fractional.

Русский

Максимум двух дробных идеалов равен их сумме и является дробным.

LaTeX

$$Max (I,J) = I ⊔ J ∧ IsFractional S (I ⊔ J)$$

Lean4

instance : Max (FractionalIdeal S P) :=
  ⟨fun I J => ⟨I ⊔ J, I.isFractional.sup J.isFractional⟩⟩

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

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

Разделы

Аффилиация

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