vsub_vadd_eq_vsub_sub — Mathlib

English

For p1,p2 ∈ P and g ∈ G, p1 -ᵥ (g +ᵥ p2) = p1 -ᵥ p2 - g.

Русский

Для p1,p2 ∈ P и g ∈ G: p1 -ᵥ (g +ᵥ p2) = p1 -ᵥ p2 - g.

LaTeX

$$$p_1 -ᵥ (g +ᵥ p_2) = p_1 -ᵥ p_2 - g$$$

Lean4

/-- Subtracting the result of adding a group element produces the same result
as subtracting the points and subtracting that group element. -/
theorem vsub_vadd_eq_vsub_sub (p₁ p₂ : P) (g : G) : p₁ -ᵥ (g +ᵥ p₂) = p₁ -ᵥ p₂ - g := by
  rw [← add_right_inj (p₂ -ᵥ p₁ : G), vsub_add_vsub_cancel, ← neg_vsub_eq_vsub_rev, vadd_vsub, ← add_sub_assoc, ←
    neg_vsub_eq_vsub_rev, neg_add_cancel, zero_sub]

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