add_modEq_left

Mathlib.Data.Int.ModEq

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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