feat(algebra/add_torsor): vsub_vadd_comm (#3928)
feat(algebra/add_torsor): vsub_vadd_comm (#3928)

Add another (commutative) `add_torsor` rearrangement lemma.






leanprover-community/mathlib,leanprover-community/mathlib