isCoprime_mul_units_right — Mathlib

English

Let u and v be units in a commutative ring R. Then y·u and z·v are coprime if and only if y and z are coprime.

Русский

Пусть u и v — единицы кольца R. Тогда y·u и z·v взаимно просты тогда и только тогда, когда y и z взаимно просты.

LaTeX

$$$\mathrm{IsCoprime}(y \cdot u, z \cdot v) \iff \mathrm{IsCoprime}(y, z)$$$

Lean4

theorem isCoprime_mul_units_right (hu : IsUnit u) (hv : IsUnit v) (y z : R) :
    IsCoprime (y * u) (z * v) ↔ IsCoprime y z :=
  Iff.trans (isCoprime_mul_unit_right_left hu _ _) (isCoprime_mul_unit_right_right hv _ _)

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