dvd_of_dvd_mul_left_of_isPrimal — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem dvd_of_dvd_mul_left_of_isPrimal (H1 : IsRelPrime x y) (H2 : x ∣ y * z) (h : IsPrimal x) : x ∣ z :=
  H1.dvd_of_dvd_mul_right_of_isPrimal (mul_comm y z ▸ H2) h

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