isRelPrime_mul_unit_left — Mathlib

English

If x is a unit, then IsRelPrime((x·y),(x·z)) is equivalent to IsRelPrime(y,z).

Русский

Если x — единица, то взаимная простота IsRelPrime((x·y),(x·z)) равносильна IsRelPrime(y,z).

LaTeX

$$$\text{IsUnit}(x) \implies \text{IsRelPrime}(x \cdot y, x \cdot z) \iff \text{IsRelPrime}(y,z)$$$

Lean4

theorem isRelPrime_mul_unit_left : IsRelPrime (x * y) (x * z) ↔ IsRelPrime y z := by
  rw [isRelPrime_mul_unit_left_left hu, isRelPrime_mul_unit_left_right hu]

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