gcd_eq_one_iff

Mathlib.Algebra.GCDMonoid.Basic

URI: https://scilib.ai/kg/mathlib#Irreducible.gcd_eq_one_iff

← MathLib Explorer

English

For irreducible x, gcd(x,y) = 1 iff not (x ∣ y).

Русский

Для неприводимого x, gcd(x,y) = 1 тогда и только если не выполняется x | y.

LaTeX

$$$gcd x y = 1 \\iff ¬(x \\mid y)$$$

Lean4

theorem gcd_eq_one_iff [NormalizedGCDMonoid α] {x y : α} (hx : Irreducible x) : gcd x y = 1 ↔ ¬(x ∣ y) := by
  rw [← hx.isUnit_gcd_iff, ← normalize_eq_one, NormalizedGCDMonoid.normalize_gcd]

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

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

Разделы

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

Аффилиация

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