isCoprime_mul_unit_left — Mathlib

English

If x is a unit, multiplying both arguments by x preserves coprimeness: IsCoprime(xy, xz) is equivalent to IsCoprime(y, z).

Русский

Если x — единица, умножение обеих компонент на x сохраняет взаимную простоту: IsCoprime(xy, xz) ⇔ IsCoprime(y, z).

LaTeX

$$$\mathrm{IsCoprime}(x y, x z) \iff \mathrm{IsCoprime}(y, z)$$$

Lean4

theorem isCoprime_mul_unit_left (hu : IsUnit x) (y z : R) : IsCoprime (x * y) (x * z) ↔ IsCoprime y z :=
  isCoprime_mul_units_left hu hu _ _

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