gcd_mul_of_coprime_of_dvd — Mathlib

English

Let a, b, c be natural numbers with gcd(a, c) = 1 and b divides c. Then gcd(a b, c) = b.

Русский

Пусть a, b, c натуральныe, gcd(a, c) = 1 и b делит c. Тогда gcd(a b, c) = b.

LaTeX

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

Lean4

theorem gcd_mul_of_coprime_of_dvd {a b c : ℕ} (hac : Coprime a c) (b_dvd_c : b ∣ c) : gcd (a * b) c = b :=
  by
  rcases exists_eq_mul_left_of_dvd b_dvd_c with ⟨d, rfl⟩
  rw [gcd_mul_right]
  convert one_mul b
  exact Coprime.coprime_mul_right_right hac

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