add_coprime_iff_right

Mathlib.Data.Nat.GCD.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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