add_mul_left_left

Mathlib.RingTheory.Coprime.Basic

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

theorem add_mul_left_left (h : IsRelPrime x y) (z : R) : IsRelPrime (x + y * z) y :=
  @of_add_mul_left_left R _ _ _ (-z) <| by simpa only [mul_neg, add_neg_cancel_right] using h

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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