Theorem equiv.of_bijective_to_fun
Modification history
2020-06-10 12:49
src/data/equiv/basic.lean
chore(data/equiv/basic): add many docstrings, review (#3008) …
Deleted equiv.of_bijective_to_funView on Github →2020-05-27 08:57
src/data/equiv/basic.lean
chore(data/equiv/basic): simplify some defs, add `coe` lemmas (#2835) …
Modified equiv.of_bijective_to_funView on Github →