isRelPrime_mul_unit_left_right — Mathlib

English

Let α be a commutative monoid and x,y,z ∈ α with x a unit. Then y and x·z are relatively prime to each other iff y and z are relatively prime.

Русский

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

LaTeX

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

Lean4

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

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