English
The gcd operation is associative up to association: gcd(gcd(m,n),k) is associated to gcd(m,gcd(n,k)).
Русский
Операция gcd ассоциативна до ассоциации: 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 [NormalizedGCDMonoid α] (m n k : α) : gcd (gcd m n) k = gcd m (gcd n k) :=
dvd_antisymm_of_normalize_eq (normalize_gcd _ _) (normalize_gcd _ _)
(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)))
