sub_modEq_iff_modEq_add

Mathlib.Algebra.ModEq

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

English

a − b ≡ c (mod p) iff a ≡ c + b (mod p).

Русский

a − b ≡ c (mod p) тогда и только тогда, когда a ≡ c + b (mod p).

LaTeX

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

Lean4

theorem sub_modEq_iff_modEq_add : a - b ≡ c [PMOD p] ↔ a ≡ c + b [PMOD p] :=
  modEq_comm.trans <| modEq_sub_iff_add_modEq.trans modEq_comm

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

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

Разделы

Аффилиация

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