Def equiv.prod_congr
Modification history
2020-10-28 15:21
src/data/equiv/basic.lean
feat(equiv/basic): use @[simps] (#4652) …
Modified equiv.prod_congrView 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.prod_congrView on Github →2020-03-29 00:11
src/data/equiv/basic.lean
feat(category/equiv_functor): type-level functoriality w.r.t. equiv (#2255) …
Modified equiv.prod_congrView on Github →2019-07-11 13:58
src/data/equiv/basic.lean
refactor(*): change priority of \simeq (#1210) …
Modified equiv.prod_congrView on Github →