Def alg_equiv.simps.symm_apply

Modification history

2022-12-09 09:32
src/algebra/algebra/basic.lean
refactor(algebra/algebra): split alg_hom and alg_equiv to separate files (#17868) …
Modified alg_equiv.simps.symm_applyView on Github →
2021-04-09 04:34
src/algebra/algebra/basic.lean
feat(tactic/simps): allow composite projections (#7074) …
Added alg_equiv.simps.symm_applyView on Github →