sub_left'

Mathlib.Data.Nat.ModEq

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

English

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

Русский

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

LaTeX

$$$ (b \le a \Leftrightarrow c \le a) \land (b \equiv c \pmod{n}) \Rightarrow a - b \equiv a - c \pmod{n} $$$

Lean4

protected theorem sub_left' (h : b ≤ a ↔ c ≤ a) (hbc : b ≡ c [MOD n]) : a - b ≡ a - c [MOD n] :=
  .sub' h .rfl hbc

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

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

Разделы

Аффилиация

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