Commit 2023-02-14 22:42 bc10e01a

View on Github →

fix: fix simp lemmas about coercion to function (#2270)

Estimated changes

added theorem MulEquiv.coe_mk
added theorem MulEquiv.coe_toEquiv
modified theorem MulEquiv.coe_toMulHom
modified theorem MulEquiv.invFun_eq_symm
modified theorem MulEquiv.symm_symm
added theorem MonoidHom.toFun_eq_coe
added theorem MulHom.toFun_eq_coe
added theorem OneHom.toFun_eq_coe
modified theorem LinearEquiv.toFun_eq_coe
added theorem LinearMap.coe_toAddHom
added theorem LinearMap.toFun_eq_coe
deleted theorem LinearMap.to_fun_eq_coe