mathlib
c83b0f33 - `coe_fn_coe_base` doesn't need to be removed from the simp set anymore

Commit
4 years ago
`coe_fn_coe_base` doesn't need to be removed from the simp set anymore
Author
Committer
Parents
Loading