mathlib

10d4811e - feat(algebra/add_torsor): injectivity lemmas (#3767)

feat(algebra/add_torsor): injectivity lemmas (#3767) Add variants of the `add_action` and `add_torsor` cancellation lemmas whose conclusion is stated in terms of `function.injective`.