mul_dvd_of_left_isPrimal — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem mul_dvd_of_left_isPrimal (H : IsRelPrime x y) (H1 : x ∣ z) (H2 : y ∣ z) (hx : IsPrimal x) : x * y ∣ z := by
  rw [mul_comm]; exact H.symm.mul_dvd_of_right_isPrimal H2 H1 hx

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