isCoprime_iff

Mathlib.RingTheory.Coprime.Basic

URI: https://scilib.ai/kg/mathlib#PNat.isCoprime_iff

← MathLib Explorer

English

For m,n ∈ ℕ+, IsCoprime m.val n.val ↔ m = 1 ∨ n = 1.

Русский

Для m,n ∈ ℕ+, IsCoprime(m.val, n.val) эквивалентно m = 1 или n = 1.

LaTeX

$$$\operatorname{IsCoprime}(m, n) \iff m = 1 \lor n = 1$$$

Lean4

/-- `IsCoprime` is not a useful definition for `PNat`; consider using `Nat.Coprime` instead. -/
theorem isCoprime_iff {m n : ℕ+} : IsCoprime (m : ℕ) n ↔ m = 1 ∨ n = 1 := by simp

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

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

Разделы

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

Аффилиация

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