mul_add_left_left_iff — Mathlib

English

Let R be a commutative ring and x, y, z ∈ R. Then x is coprime to y if and only if yz + x is coprime to y.

Русский

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

LaTeX

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

Lean4

theorem mul_add_left_left_iff {x y z : R} : IsRelPrime (y * z + x) y ↔ IsRelPrime x y :=
  ⟨of_mul_add_left_left, fun h ↦ h.mul_add_left_left z⟩

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