isRelPrime_mul_unit_right — Mathlib

English

If x is a unit and y,z are such that IsRelPrime(xy,z) and IsRelPrime(xz,y) hold, then IsRelPrime(y,z) is equivalent to IsRelPrime(xy,xz).

Русский

Если x — единица и IsRelPrime(xy,z) и IsRelPrime(xz,y) выполняются, то IsRelPrime(y,z) эквивалентно IsRelPrime(xy,xz).

LaTeX

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

Lean4

theorem isRelPrime_mul_unit_right : IsRelPrime (y * x) (z * x) ↔ IsRelPrime y z := by
  rw [isRelPrime_mul_unit_right_left hu, isRelPrime_mul_unit_right_right hu]

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