mul_add_left_right_iff — Mathlib

English

Let R be a commutative ring and x, y, z ∈ R. Then IsRelPrime x (x*z + y) is equivalent to IsRelPrime x y.

Русский

Пусть R — коммутативное кольцо и x, y, z ∈ R. Тогда IsRelPrime x (xz + y) эквивалентно IsRelPrime x y.

LaTeX

$$$IsRelPrime\\left(x, x \\cdot z + y\\right) \\iff IsRelPrime(x, y)$$$

Lean4

theorem mul_add_left_right_iff {x y z : R} : IsRelPrime x (x * z + y) ↔ IsRelPrime x y :=
  ⟨of_mul_add_left_right, fun h ↦ h.mul_add_left_right z⟩

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