modEq_sub_fac

Mathlib.Data.Int.ModEq

URI: https://scilib.ai/kg/mathlib#Int.modEq_sub_fac

← MathLib Explorer

English

If a ≡ b [ZMOD n], then a − n·c ≡ b [ZMOD n].

Русский

Если a ≡ b [ZMOD n], то a − n·c ≡ b [ZMOD n].

LaTeX

$$$\\forall a,b,n,c \\in \\mathbb{Z},\\; a \\equiv b [ZMOD n] \\Rightarrow a - n \\cdot c \\equiv b [ZMOD n].$$$

Lean4

theorem modEq_sub_fac {a b n : ℤ} (c : ℤ) (ha : a ≡ b [ZMOD n]) : a - n * c ≡ b [ZMOD n] := by
  convert Int.modEq_add_fac (-c) ha using 1; rw [Int.mul_neg, sub_eq_add_neg]

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

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

Разделы

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

Аффилиация

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