mul_left — Mathlib

English

If x is coprime to z and y is coprime to z, then xy is coprime to z.

Русский

Если x взаимно простo z и y взаимно простo z, тогда xy взаимно простo z.

LaTeX

$$$IsCoprime(x,z) \land IsCoprime(y,z) \Rightarrow IsCoprime(x\cdot y, z)$$$

Lean4

theorem mul_left (H1 : IsCoprime x z) (H2 : IsCoprime y z) : IsCoprime (x * y) z :=
  let ⟨a, b, h1⟩ := H1
  let ⟨c, d, h2⟩ := H2
  ⟨a * c, a * x * d + b * c * y + b * d * z,
    calc
      a * c * (x * y) + (a * x * d + b * c * y + b * d * z) * z
      _ = (a * x + b * z) * (c * y + d * z) := by ring
      _ = 1 := by rw [h1, h2, mul_one]⟩

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