Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-11-24 20:38 13fedc15

View on Github →

feat(algebra/group): define mul/add_left/right_injective (#1730) Same as mul_left_cancel etc but uses function.injective. This makes it easier to use functions from function.injective namespace.

Estimated changes