isRelPrime_mul_unit_left_left — Mathlib

English

Let α be a commutative monoid and x,y,z ∈ α with x a unit. Then x·y and z are relatively prime if and only if y and z are relatively prime.

Русский

Пусть α — коммутативное монотное множество, и элементы x, y, z ∈ α таковы, что x — единица. Тогда x·y и z взаимно просты тогда и только тогда, когда y и z взаимно просты.

LaTeX

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

Lean4

theorem isRelPrime_mul_unit_left_left : IsRelPrime (x * y) z ↔ IsRelPrime y z :=
  ⟨IsRelPrime.of_mul_left_right, fun H _ h ↦ H (hu.dvd_mul_left.mp h)⟩

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