coprime_add_self_left

Mathlib.Data.Nat.GCD.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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