dvd_mul_gcd_of_dvd_mul — Mathlib

English

If α is a nonempty gcd-monoid, then every divisor k of a product m n can be written as a product m' n' where m' | m and n' | n.

Русский

Если α - непустой gcd-монойд, то любой делитель k произведения m n записывается как произведение m' n', причём m' делит m, а n' делит n.

LaTeX

$$$\\text{DecompositionMonoid}(\\alpha)$ означает: если $k \\mid (m n)$, то существуют $m'$, $n'$ такие, что $m' \\mid m$, $n' \\mid n$ и $k = m' n'$.$$

Lean4

theorem dvd_mul_gcd_of_dvd_mul [GCDMonoid α] {m n k : α} (H : k ∣ m * n) : k ∣ m * gcd k n :=
  by
  rw [mul_comm] at H ⊢
  exact dvd_gcd_mul_of_dvd_mul H

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