Commit 2020-08-15 14:12 10d4811e

View on Github →

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.

Estimated changes

Modified src/algebra/add_torsor.lean

added theorem vadd_left_injective

added theorem vadd_right_injective

added theorem vsub_left_injective

added theorem vsub_right_injective