sub_iff_left — Mathlib

English

If a₁ ≡ b₁ (mod p), then a₁ − a₂ ≡ b₁ − b₂ (mod p) is equivalent to a₂ ≡ b₂ (mod p).

Русский

Если a₁ ≡ b₁ (mod p), то a₁ − a₂ ≡ b₁ − b₂ (mod p) эквивалентно a₂ ≡ b₂ (mod p).

LaTeX

$$$ a_1 \\equiv b_1 \\pmod{p} \\;\\Rightarrow\\; \\big( a_1 - a_2 \\equiv b_1 - b_2 \\pmod{p} \\ \\iff\\; a_2 \\equiv b_2 \\pmod{p} \\big) $$$

Lean4

@[simp]
protected theorem sub_iff_left : a₁ ≡ b₁ [PMOD p] → (a₁ - a₂ ≡ b₁ - b₂ [PMOD p] ↔ a₂ ≡ b₂ [PMOD p]) := fun ⟨m, hm⟩ =>
  (Equiv.subLeft m).symm.exists_congr_left.trans <| by simp [sub_sub_sub_comm, hm, sub_smul, ModEq]

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