coprime_sub_self_left

Mathlib.Data.Nat.GCD.Basic

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

English

If m ≤ n, then Coprime(n−m, m) ↔ Coprime(n, m).

Русский

Пусть m ≤ n. Тогда gcd(n−m, m) = 1 эквивалентно gcd(n, m) = 1.

LaTeX

$$$$\forall m,n \in \mathbb{N}, m \le n \Rightarrow \gcd(n-m, m) = 1 \iff \gcd(n, m) = 1$$$$

Lean4

@[simp]
theorem coprime_sub_self_left {m n : ℕ} (h : m ≤ n) : Coprime (n - m) m ↔ Coprime n m := by
  rw [Coprime, Coprime, gcd_sub_self_left h]

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

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

Разделы

Аффилиация

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