mathlib
62655a23 - chore(data/dfinsupp): add the simp lemma coe_pre_mk (#7806)

Commit

4 years ago

chore(data/dfinsupp): add the simp lemma coe_pre_mk (#7806)

Author

eric-wieser

eric-wieser

Parents

Loading