add_left_cancel'

Mathlib.Data.Nat.ModEq

URI: https://scilib.ai/kg/mathlib#Nat.ModEq.add_left_cancel'

English

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

Русский

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

LaTeX

$$$(c + a) \\equiv (c + b) \\pmod{n} \\Rightarrow a \\equiv b \\pmod{n}$$$

Lean4

protected theorem add_left_cancel' (c : ℕ) (h : c + a ≡ c + b [MOD n]) : a ≡ b [MOD n] :=
  ModEq.rfl.add_left_cancel h

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

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

Разделы

Аффилиация

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