neg_modEq_neg

Mathlib.Data.Int.ModEq

URI: https://scilib.ai/kg/mathlib#Int.neg_modEq_neg

English

Let a, b, n be integers. Then -a ≡ -b (mod n) if and only if a ≡ b (mod n).

Русский

Пусть a, b, n — целые числа. Тогда -a ≡ -b (mod n) если и только a ≡ b (mod n).

LaTeX

$$$-a \equiv -b \pmod n \iff a \equiv b \pmod n$$$

Lean4

@[simp]
theorem neg_modEq_neg : -a ≡ -b [ZMOD n] ↔ a ≡ b [ZMOD n] := by
  simp only [modEq_iff_dvd, (by cutsat : -b - -a = -(b - a)), Int.dvd_neg]

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

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

Разделы

Аффилиация

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