mathlib
2ce95ca8 - refactor(data/finsupp): use `{f : α →₀ M | ∃ a b, f = single a b}` instead of union of ranges (#10671)

Commit

4 years ago

refactor(data/finsupp): use `{f : α →₀ M | ∃ a b, f = single a b}` instead of union of ranges (#10671)

Author

urkud

Parents