Structure equiv
Modification history
2022-10-18 21:51
src/logic/equiv/basic.lean
chore(logic/equiv/basic): split into two files (#17038) …
Modified equivView on Github →2022-08-21 09:59
test/simps.lean
feat(algebra/*): Algebraic instances on `lex`/`order_dual` (#16122) …
Deleted equivView on Github →2020-04-18 00:48
test/lint_coe_to_fun.lean
feat(tactic/lint): lint for missing has_coe_to_fun instances (#2437) …
Added equivView on Github →2019-12-09 20:49
test/tactics.lean
A `ring_exp` tactic for dealing with exponents in rings (#1715) …
Deleted equivView on Github →