add_coprime_iff_left

Mathlib.Data.Nat.GCD.Basic

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

English

If c divides b, then Coprime(a+b, c) ⇔ Coprime(a, c).

Русский

Если c делит b, тогда Coprime(a+b, c) эквивалентно Coprime(a, c).

LaTeX

$$$$\forall a,b,c \in \mathbb{N}, c \mid b \Rightarrow \gcd(a+b, c) = 1 \iff \gcd(a, c) = 1$$$$

Lean4

theorem add_coprime_iff_left (h : c ∣ b) : Coprime (a + b) c ↔ Coprime a c := by obtain ⟨n, rfl⟩ := h; simp

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

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

Разделы

Аффилиация

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