add_modEq_right

Mathlib.Algebra.ModEq

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem add_modEq_right : a + b ≡ b [PMOD p] ↔ a ≡ 0 [PMOD p] := by
  simp [← modEq_sub_iff_add_modEq]
    -- this matches `Int.modEq_iff_add_fac`

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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