Commit 2020-05-23 07:44 8c1793fe
View on Github →chore(data/equiv): make equiv.ext args use { } (#2776)
Other changes:
- rename lemmas
eq_of_to_fun_eqtocoe_fn_injective; - add
left_inverse.eq_right_inverseand use it to proveequiv.ext.
chore(data/equiv): make equiv.ext args use { } (#2776)
Other changes:
eq_of_to_fun_eq to coe_fn_injective;left_inverse.eq_right_inverse and use it to prove equiv.ext.