isCoprime_iff_sup_eq

Mathlib.RingTheory.Ideal.Operations

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

English

IsCoprime I J is equivalent to I ⊔ J = ⊤.

Русский

IsCoprime I J эквивалентно I ⊔ J = ⊤.

LaTeX

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

Lean4

theorem isCoprime_iff_sup_eq : IsCoprime I J ↔ I ⊔ J = ⊤ := by rw [isCoprime_iff_codisjoint, codisjoint_iff]

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

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

Разделы

Аффилиация

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