sub — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[gcongr]
protected theorem sub (hca : c ≤ a) (hdb : d ≤ b) (hab : a ≡ b [MOD n]) (hcd : c ≡ d [MOD n]) : a - c ≡ b - d [MOD n] :=
  .sub' (iff_of_true hca hdb) hab hcd

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