add_mul_right_left

Mathlib.RingTheory.Coprime.Basic

URI: https://scilib.ai/kg/mathlib#IsRelPrime.add_mul_right_left

English

If IsRelPrime x y, then for any z, IsRelPrime (x + z*y) y.

Русский

Если IsRelPrime x y, то для любого z верно IsRelPrime(x + z*y, y).

LaTeX

$$$\operatorname{IsRelPrime}(x, y) \Rightarrow \operatorname{IsRelPrime}(x + z \cdot y, y)$$$

Lean4

theorem add_mul_right_left (h : IsRelPrime x y) (z : R) : IsRelPrime (x + z * y) y :=
  mul_comm z y ▸ h.add_mul_left_left z

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru