neg_right_iff

Mathlib.RingTheory.Coprime.Basic

URI: https://scilib.ai/kg/mathlib#IsCoprime.neg_right_iff

English

IsCoprime(x, -y) is equivalent to IsCoprime(x, y).

Русский

IsCoprime(x, -y) эквивалентно IsCoprime(x, y).

LaTeX

$$$\mathrm{IsCoprime}(x, -y) \iff \mathrm{IsCoprime}(x, y)$$$

Lean4

theorem neg_right_iff (x y : R) : IsCoprime x (-y) ↔ IsCoprime x y :=
  ⟨fun h => neg_neg y ▸ h.neg_right, neg_right⟩

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

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

Разделы

Аффилиация

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