lcm_eq_inf

Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

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

English

In a Dedekind domain, the least common multiple equals the infimum (intersection): lcm(I,J) = I ⊓ J.

Русский

В области Дедекина наименьшее общее кратное равно пересечению: lcm(I,J) = I ⊓ J.

LaTeX

$$lcm(I,J) = I ⊓ J$$

Lean4

@[simp]
theorem lcm_eq_inf (I J : Ideal A) : lcm I J = I ⊓ J :=
  rfl

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

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

Разделы

Аффилиация

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