mathlib
35b835a2 - feat(data/set/sigma): Indexed sum of sets (#12305)

Commit
3 years ago
feat(data/set/sigma): Indexed sum of sets (#12305) Define `set.sigma`, the sum of a family of sets indexed by a set.
Author
Parents
Loading