mul_left — Mathlib

English

If x and y are each relatively prime to z, then their product is relatively prime to z.

Русский

Если x и y взаимно просты к z, то их произведение взаимно просто с z.

LaTeX

$$$\text{IsRelPrime}(x,z) \rightarrow \text{IsRelPrime}(y,z) \rightarrow \text{IsRelPrime}(x \cdot y, z)$$$

Lean4

theorem mul_left (H1 : IsRelPrime x z) (H2 : IsRelPrime y z) : IsRelPrime (x * y) z := fun _ h hz ↦
  by
  obtain ⟨a, b, ha, hb, rfl⟩ := exists_dvd_and_dvd_of_dvd_mul h
  exact (H1 ha <| (dvd_mul_right a b).trans hz).mul (H2 hb <| (dvd_mul_left b a).trans hz)

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