pointwise): Missing `smul_comm_class` instances (#14963)

Commit

3 years ago

feat({data/{finset,set},order/filter}/pointwise): Missing `smul_comm_class` instances (#14963) Instances of the form `smul_comm_class α β (something γ)`.

Author

YaelDillies

Parents

32b08ef8

mathlib ee7a8863 - feat({data/{finset,set},order/filter}/pointwise): Missing `smul_comm_class` instances (#14963)

mathlib
ee7a8863 - feat({data/{finset,set},order/filter}/pointwise): Missing `smul_comm_class` instances (#14963)