gcd — Mathlib

English

If a1 is associated to a2 and b1 is associated to b2, then gcd(a1,b1) is associated to gcd(a2,b2).

Русский

Если a1 ассоциировано c a2 и b1 ассоциировано c b2, то gcd(a1,b1) ассоциировано с gcd(a2,b2).

LaTeX

$$$$ \text{Associated}(a_1,a_2) \land \text{Associated}(b_1,b_2) \Rightarrow \text{Associated}(\gcd(a_1,b_1), \gcd(a_2,b_2)). $$$$

Lean4

protected theorem gcd [GCDMonoid α] {a₁ a₂ b₁ b₂ : α} (ha : Associated a₁ a₂) (hb : Associated b₁ b₂) :
    Associated (gcd a₁ b₁) (gcd a₂ b₂) :=
  associated_of_dvd_dvd (gcd_dvd_gcd ha.dvd hb.dvd) (gcd_dvd_gcd ha.dvd' hb.dvd')

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