vadd_eq_vadd_iff_neg_add_eq_vsub — Mathlib

English

For all v1,v2 ∈ G and p1,p2 ∈ P, v1 +ᵥ p1 = v2 +ᵥ p2 iff -v1 + v2 = p1 -ᵥ p2.

Русский

Для всех v1,v2 ∈ G и p1,p2 ∈ P: v1 +ᵥ p1 = v2 +ᵥ p2 ⇔ -v1 + v2 = p1 -ᵥ p2.

LaTeX

$$$v_1 +ᵥ p_1 = v_2 +ᵥ p_2 \iff -v_1 + v_2 = p_1 -ᵥ p_2$$$

Lean4

theorem vadd_eq_vadd_iff_neg_add_eq_vsub {v₁ v₂ : G} {p₁ p₂ : P} : v₁ +ᵥ p₁ = v₂ +ᵥ p₂ ↔ -v₁ + v₂ = p₁ -ᵥ p₂ := by
  rw [eq_vadd_iff_vsub_eq, vadd_vsub_assoc, ← add_right_inj (-v₁), neg_add_cancel_left, eq_comm]

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