Commit 2024-10-08 17:07 641e6550

View on Github →

feat: order properties of Finsupp.single (#17461) From LeanCamCombi

Estimated changes

Modified Mathlib/Data/Finsupp/Order.lean

added theorem Finsupp.mapDomain_mono

added theorem Finsupp.mapDomain_nonneg

added theorem Finsupp.mapDomain_nonpos

added theorem Finsupp.single_le_single

added theorem Finsupp.single_mono

added theorem Finsupp.single_nonneg

added theorem Finsupp.single_nonpos

added theorem Finsupp.sum_le_sum

added theorem Finsupp.sum_le_sum_index