sub_iff_right — 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_2 \\equiv b_2 \\pmod{p} \\;\\Rightarrow\\; \\big( a_1 - a_2 \\equiv b_1 - b_2 \\pmod{p} \\ \\iff\\; a_1 \\equiv b_1 \\pmod{p} \\big) $$$

Lean4

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

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