mathlib3
2c273240 - add `mul_mem_coe` to help with elaboration

Commit

3 years ago

add `mul_mem_coe` to help with elaboration

References

j-loreaux/mul-mem

Author

j-loreaux

j-loreaux

Parents

Loading