modEq_sub_iff_add_modEq

Mathlib.Algebra.ModEq

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

English

A ≡ B − C (mod p) iff A + C ≡ B (mod p).

Русский

A ≡ B − C (mod p) эквивалентно A + C ≡ B (mod p).

LaTeX

$$$ a \\equiv b - c \\pmod{p} \\iff a + c \\equiv b \\pmod{p} $$$

Lean4

theorem modEq_sub_iff_add_modEq : a ≡ b - c [PMOD p] ↔ a + c ≡ b [PMOD p] :=
  modEq_sub_iff_add_modEq'.trans <| by rw [add_comm]

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

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

Разделы

Аффилиация

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