mathlib
1404ad83 - feat(algebra/add_torsor): vsub_vadd_comm (#3928)

Commit

5 years ago

feat(algebra/add_torsor): vsub_vadd_comm (#3928) Add another (commutative) `add_torsor` rearrangement lemma.

References

Author

jsm28

Parents