lcm — Mathlib

English

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

Русский

Если a1 ассоциирован с a2 и b1 ассоциирован с b2, тогда lcm(a1,b1) ассоциирован с lcm(a2,b2).

LaTeX

$$$ \operatorname{Associated}(a_1,b_2) \Rightarrow \operatorname{Associated}(\operatorname{lcm}(a_1,b_1), \operatorname{lcm}(a_2,b_2)) $$$

Lean4

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

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