mul_dvd_of_right_isPrimal — Mathlib

English

If x and y are relatively prime, x divides z, y divides z, and y is primal, then x·y divides z.

Русский

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

LaTeX

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

Lean4

theorem mul_dvd_of_right_isPrimal (H : IsRelPrime x y) (H1 : x ∣ z) (H2 : y ∣ z) (hy : IsPrimal y) : x * y ∣ z :=
  by
  obtain ⟨w, rfl⟩ := H1
  exact mul_dvd_mul_left x (H.symm.dvd_of_dvd_mul_left_of_isPrimal H2 hy)

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