English
The equation p1 = g +ᵥ p2 is equivalent to p1 -ᵥ p2 = g.
Русский
Уравнение p1 = g +ᵥ p2 эквивалентно p1 -ᵥ p2 = g.
LaTeX
$$$p_1 = g +ᵥ p_2 \iff p_1 -ᵥ p_2 = g$$$
Lean4
/-- Convert between an equality with adding a group element to a point
and an equality of a subtraction of two points with a group
element. -/
theorem eq_vadd_iff_vsub_eq (p₁ : P) (g : G) (p₂ : P) : p₁ = g +ᵥ p₂ ↔ p₁ -ᵥ p₂ = g :=
⟨fun h => h.symm ▸ vadd_vsub _ _, fun h => h ▸ (vsub_vadd _ _).symm⟩