finsets (#11355)

Commit

4 years ago

feat(data/{multiset,finset}/sum): Disjoint sum of multisets/finsets (#11355) This defines the disjoint union of two multisets/finsets as `multiset (α ⊕ β)`/`finset (α ⊕ β)`.

Author

YaelDillies

Parents

9a949936

mathlib 85accb8a - feat(data/{multiset,finset}/sum): Disjoint sum of multisets/finsets (#11355)

mathlib
85accb8a - feat(data/{multiset,finset}/sum): Disjoint sum of multisets/finsets (#11355)