Commit 2025-08-03 14:43 dce8c77c

feat(Algebra/AddTorsor/Basic) vadd_vsub_vadd_comm (#27865) Add vadd_vsub_vadd_comm

theorem vadd_vsub_vadd_comm (v₁ v₂ : G) (p₁ p₂ : P) : (v₁ +ᵥ p₁) -ᵥ (v₂ +ᵥ p₂) = (v₁ - v₂)
    + (p₁ -ᵥ p₂) := by
  rw [vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, add_sub_assoc, ← add_comm_sub]