gcd_dvd_gcd_mul_right_right — Mathlib

English

Let α be a gcd-monoid with cancellation. For all m,n,k in α, gcd(m,n) divides gcd(m, n k).

Русский

Пусть α — моноид с НОД и свойством отмены. Для любых m, n, k в α выполнено gcd(m,n) делится на gcd(m, n k).

LaTeX

$$$\\\\forall m n k : \\\\alpha, \\\\gcd m n \\\\mid \\\\gcd m (n k)$$$

Lean4

theorem gcd_dvd_gcd_mul_right_right [GCDMonoid α] (m n k : α) : gcd m n ∣ gcd m (n * k) := by grw [← dvd_mul_right]

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