mathlib3
2f939e93 - chore(data/equiv/basic): redefine `set.bij_on.equiv` (#5128)

Commit
5 years ago
chore(data/equiv/basic): redefine `set.bij_on.equiv` (#5128) Now `set.bij_on.equiv` works for any `h : set.bij_on f s t`. The old behaviour can be achieved using `(equiv.set_univ _).symm.trans _`.
Author
Parents
Loading