mathlib
383dd2bd - chore(data/equiv): add missing simp lemmas about mk (#6505)

Commit

4 years ago

chore(data/equiv): add missing simp lemmas about mk (#6505) This adds missing `mk_coe` lemmas, and new `symm_mk`, `symm_bijective`, and `mk_coe'` lemmas.

Author

eric-wieser

Parents

22e34370

mathlib 383dd2bd - chore(data/equiv): add missing simp lemmas about mk (#6505)

mathlib
383dd2bd - chore(data/equiv): add missing simp lemmas about mk (#6505)