gcd_mul_gcd_eq_iff_dvd_mul_of_coprime

English

Let n and m be coprime. For any x, gcd(x,n) gcd(x,m) = x if and only if x is a multiple of n m.

Русский

Пусть n и m взаимно просты. Для любого x gcd(x,n) gcd(x,m) = x тогда и только тогда x делится на n m.

LaTeX

$$$\forall x,n,m \in \mathbb{N}, \gcd(n,m)=1 \Rightarrow (\gcd(x,n) \cdot \gcd(x,m) = x) \iff x \mid (n m)$$$

Lean4

theorem gcd_mul_gcd_eq_iff_dvd_mul_of_coprime (hcop : Coprime n m) : gcd x n * gcd x m = x ↔ x ∣ n * m :=
  by
  refine ⟨fun h ↦ ?_, (dvd_antisymm ?_ <| dvd_gcd_mul_gcd_iff_dvd_mul.mpr ·)⟩
  refine h ▸ Nat.mul_dvd_mul ?_ ?_ <;> exact x.gcd_dvd_right _
  refine (hcop.gcd_both x x).mul_dvd_of_dvd_of_dvd ?_ ?_ <;> exact x.gcd_dvd_left _

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