isCoprime_iff_gcd

Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

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

← MathLib Explorer

English

Two ideals I,J are coprime if and only if gcd(I,J) = 1.

Русский

Идеалы I и J являются взаимно простыми тогда и только если их НОД равен единице.

LaTeX

$$IsCoprime(I,J) \\iff gcd(I,J) = 1$$

Lean4

theorem isCoprime_iff_gcd {I J : Ideal A} : IsCoprime I J ↔ gcd I J = 1 := by
  rw [Ideal.isCoprime_iff_codisjoint, codisjoint_iff, one_eq_top, gcd_eq_sup]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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