sub

Mathlib.Data.Int.ModEq

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

@[gcongr]
protected theorem sub (h₁ : a ≡ b [ZMOD n]) (h₂ : c ≡ d [ZMOD n]) : a - c ≡ b - d [ZMOD n] :=
  by
  rw [sub_eq_add_neg, sub_eq_add_neg]
  exact h₁.add h₂.neg

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

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

Разделы

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

Аффилиация

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