gcd_dvd_gcd_mul_left_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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