sup_eq

Mathlib.RingTheory.Ideal.Operations

URI: https://scilib.ai/kg/mathlib#IsCoprime.sup_eq

English

If IsCoprime I J, then I ⊔ J = ⊤.

Русский

Если IsCoprime I J, то I ⊔ J = ⊤.

LaTeX

$$$$ IsCoprime I J \Rightarrow I \sqcup J = \top $$$$

Lean4

theorem _root_.IsCoprime.sup_eq (h : IsCoprime I J) : I ⊔ J = ⊤ :=
  isCoprime_iff_sup_eq.mp h

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

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

Разделы

Аффилиация

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