Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-09-05 19:32 7c38416b

View on Github →

feat(data/sigma,data/finset,algebra): add support for the sigma type to finset and big operators

Estimated changes

Modified algebra/big_operators.lean

added theorem finset.prod_sigma

Modified data/finset/fold.lean

added theorem finset.mem_sigma_iff

added theorem finset.sigma_mono

added theorem heq_iff_eq

Created data/sigma/basic.lean

added def sigma.map

added theorem sigma.mk_eq_mk_iff

Created data/sigma/default.lean

Modified topology/infinite_sum.lean

modified theorem is_sum_sigma