mathlib
d3d35395 - Removed unnecessary assumption in `map_injective_of_injective` (#15184)

Commit

3 years ago

Removed unnecessary assumption in `map_injective_of_injective` (#15184) Removed assumption in `map_injective_of_injective`

Author

nick-kuhn

Parents