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 C + A ≡ B (mod p).

Русский

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

LaTeX

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

Lean4

theorem modEq_sub_iff_add_modEq' : a ≡ b - c [PMOD p] ↔ c + a ≡ b [PMOD p] := by simp [ModEq, sub_sub]

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

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

Разделы

Аффилиация

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