mathlib
50696a85 - chore(data/multiset/basic): Inline instances (#14208)

Commit
3 years ago
chore(data/multiset/basic): Inline instances (#14208) We inline various protected theorems into the `ordered_cancel_add_comm_monoid` instance. We also declare `covariant_class` and `contravariant_class` instances, which make further theorems redundant.
Author
Parents
Loading