Commit 2022-06-26 14:56 ee7a8863

View on Github →

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

Estimated changes

Modified src/data/finset/basic.lean

added theorem finset.image_comm

added theorem finset.map_comm

Modified src/data/finset/pointwise.lean

Modified src/data/set/pointwise.lean

modified theorem set.smul_set_mono

added theorem set.smul_set_subset_iff

Modified src/order/filter/pointwise.lean