add_modEq_right

Mathlib.Data.Int.ModEq

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

English

If n is an integer and a ≡ b [ZMOD n], then a + n ≡ a [ZMOD n].

Русский

Если n ∈ ℤ и a ≡ b [ZMOD n], то a + n ≡ a [ZMOD n].

LaTeX

$$$\\forall n,a,b \\in \\mathbb{Z}, \\; a \\equiv b [ZMOD n] \\Rightarrow a + n \\equiv a [ZMOD n].$$$

Lean4

@[simp]
theorem add_modEq_right : a + n ≡ a [ZMOD n] :=
  ModEq.symm <| modEq_iff_dvd.2 <| by simp

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

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

Разделы

Аффилиация

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