mul_dvd — Mathlib

English

If IsCoprime x y and x divides z and y divides z, then xy divides z.

Русский

Если IsCoprime x y и x делится на z, и y делится на z, тогда xy делит z.

LaTeX

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

Lean4

theorem mul_dvd (H : IsCoprime x y) (H1 : x ∣ z) (H2 : y ∣ z) : x * y ∣ z :=
  by
  obtain ⟨a, b, h⟩ := H
  rw [← mul_one z, ← h, mul_add]
  apply dvd_add
  · rw [mul_comm z, mul_assoc]
    exact (mul_dvd_mul_left _ H2).mul_left _
  · rw [mul_comm b, ← mul_assoc]
    exact (mul_dvd_mul_right H1 _).mul_right _

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