neg_neg_iff

Mathlib.RingTheory.Coprime.Basic

URI: https://scilib.ai/kg/mathlib#IsCoprime.neg_neg_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_neg_iff (x y : R) : IsCoprime (-x) (-y) ↔ IsCoprime x y :=
  (neg_left_iff _ _).trans (neg_right_iff _ _)

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

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

Разделы

Аффилиация

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