factor_eq_gcd_left — Mathlib

English

If cop = gcd(m,n)=1, and a|m, b|n, then a = gcd(m, a b).

Русский

Пусть cop = gcd(m,n)=1, и a делит m, b делит n, тогда a = gcd(m, a b).

LaTeX

$$$ \gcd(m, a b) = a \quad\text{при}\quad \gcd(m,n)=1, \ a|m, \ b|n $$$

Lean4

theorem factor_eq_gcd_left {a b m n : ℕ+} (cop : m.Coprime n) (am : a ∣ m) (bn : b ∣ n) : a = (a * b).gcd m :=
  by
  rw [← gcd_eq_left_iff_dvd] at am
  conv_lhs => rw [← am]
  rw [eq_comm]
  apply Coprime.gcd_mul_right_cancel a
  apply Coprime.coprime_dvd_left bn cop.symm

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