add_modEq_left

Mathlib.Algebra.ModEq

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

English

a + b ≡ a (mod p) iff b ≡ 0 (mod p).

Русский

a + b ≡ a (mod p) эквивалентно b ≡ 0 (mod p).

LaTeX

$$$ a + b \\equiv a \\pmod{p} \\iff b \\equiv 0 \\pmod{p} $$$

Lean4

@[simp]
theorem add_modEq_left : a + b ≡ a [PMOD p] ↔ b ≡ 0 [PMOD p] := by simp [← modEq_sub_iff_add_modEq']

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

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

Разделы

Аффилиация

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