gcd_eq_sup

Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

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

English

In a Dedekind domain, the gcd of two ideals equals their sum (supremum): gcd(I,J) = I ⊔ J.

Русский

В области Дедекина наибольший общий делитель идеалов равен их сумме: gcd(I,J) = I ⊔ J.

LaTeX

$$gcd(I,J) = I ⊔ J$$

Lean4

@[simp]
theorem gcd_eq_sup (I J : Ideal A) : gcd I J = I ⊔ J :=
  rfl

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

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

Разделы

Аффилиация

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