Commit 2024-12-20 05:03 5999d673

View on Github →

chore(Multiset): make all arguments to inter_le_left, etc... implicit (#20045) This follows what we already do for Set, Finset, general lattices

Estimated changes

modified theorem Multiset.inter_le_left
modified theorem Multiset.inter_le_right
modified theorem Multiset.le_union_left
modified theorem Multiset.le_union_right
modified theorem Multiset.union_add_inter
modified theorem Multiset.Nodup.inter_left
modified theorem Multiset.Nodup.inter_right