English
An Associated version of gcd associativity: Associated (gcd(gcd m n) k) (gcd m gcd(n k)).
Русский
Ассоциативность gcd в версии по ассоциации: Associated( gcd(gcd m n) k, gcd m gcd(n k) ).
LaTeX
$$$$ \\operatorname{Associated}(\\gcd(\\gcd(m,n),k), \\gcd(m, \\gcd(n,k))) $$$$
Lean4
theorem gcd_assoc' [GCDMonoid α] (m n k : α) : Associated (gcd (gcd m n) k) (gcd m (gcd n k)) :=
associated_of_dvd_dvd
(dvd_gcd ((gcd_dvd_left (gcd m n) k).trans (gcd_dvd_left m n))
(dvd_gcd ((gcd_dvd_left (gcd m n) k).trans (gcd_dvd_right m n)) (gcd_dvd_right (gcd m n) k)))
(dvd_gcd (dvd_gcd (gcd_dvd_left m (gcd n k)) ((gcd_dvd_right m (gcd n k)).trans (gcd_dvd_left n k)))
((gcd_dvd_right m (gcd n k)).trans (gcd_dvd_right n k)))
