add_right_cancel

Mathlib.Data.Int.ModEq

URI: https://scilib.ai/kg/mathlib#Int.ModEq.add_right_cancel

← MathLib Explorer

English

If c ≡ d (mod n) and a + c ≡ b + d (mod n), then a ≡ b (mod n).

Русский

Если c ≡ d (mod n) и a + c ≡ b + d (mod n), то a ≡ b (mod n).

LaTeX

$$$c \equiv d \pmod n \land a + c \equiv b + d \pmod n \Rightarrow a \equiv b \pmod n$$$

Lean4

protected theorem add_right_cancel (h₁ : c ≡ d [ZMOD n]) (h₂ : a + c ≡ b + d [ZMOD n]) : a ≡ b [ZMOD n] :=
  by
  rw [add_comm a, add_comm b] at h₂
  exact h₁.add_left_cancel h₂

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

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

Разделы

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

Аффилиация

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