Commit 2020-11-27 06:39 2f939e93
View on Github →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 _.
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 _.