Commit 2021-12-08 17:16 2ce95ca8
View on Github →refactor(data/finsupp): use {f : α →₀ M | ∃ a b, f = single a b} instead of union of ranges (#10671)
refactor(data/finsupp): use {f : α →₀ M | ∃ a b, f = single a b} instead of union of ranges (#10671)