Commit 2022-02-27 23:09 dfacfd34
View on Github →chore(linear_algebra/basic): make linear_map.id_coe elegible for dsimp (#12334)
dsimp only considers lemmas which are proved by rfl, not ones that just could be.
chore(linear_algebra/basic): make linear_map.id_coe elegible for dsimp (#12334)
dsimp only considers lemmas which are proved by rfl, not ones that just could be.