add_eq_sup

Mathlib.RingTheory.Ideal.Operations

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

English

The sum of two ideals I and J coincides with their supremum: I + J = I ⊔ J.

Русский

Сумма двух идеалов I и J совпадает с их верхой: I + J = I ⊔ J.

LaTeX

$$$I + J = I \\sqcup J$$$

Lean4

@[simp]
theorem add_eq_sup {I J : Ideal R} : I + J = I ⊔ J :=
  rfl

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

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

Разделы

Аффилиация

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