mathlib
866294d3 - fix(data/dfinsupp): fix nat- and int- module diamonds (#9299)

Commit

4 years ago

fix(data/dfinsupp): fix nat- and int- module diamonds (#9299) This also defines `has_sub` separately in case it turns out to help with unification

Author

eric-wieser

Parents