mathlib

e9b8651e - feat(data/(d)finsupp): well-foundedness of lexicographic and product orders (#16772)

feat(data/(d)finsupp): well-foundedness of lexicographic and product orders (#16772) | condition on domain | finsupp/dfinsupp | function/pi | |