coprime_add_self_right

Mathlib.Data.Nat.GCD.Basic

URI: https://scilib.ai/kg/mathlib#Nat.coprime_add_self_right

English

Coprime m (n + m) holds if and only if Coprime m n.

Русский

Coprime(m, n + m) эквивалентно Coprime(m, n).

LaTeX

$$$\text{Coprime}(m,n+m) \iff \text{Coprime}(m,n).$$$

Lean4

@[simp]
theorem coprime_add_self_right {m n : ℕ} : Coprime m (n + m) ↔ Coprime m n := by
  rw [Coprime, Coprime, gcd_add_self_right]

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

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

Разделы

Аффилиация

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