mul_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem mul_right (H1 : IsRelPrime x y) (H2 : IsRelPrime x z) : IsRelPrime x (y * z) := by
  rw [isRelPrime_comm] at H1 H2 ⊢; exact H1.mul_left H2

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