): add coe_of simp lemmas (#3938)

Commit

5 years ago

feat(*/category/*): add coe_of simp lemmas (#3938) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

References

Author

kim-em

Parents

mathlib fb6046ed - feat(*/category/*): add coe_of simp lemmas (#3938)