Mathlib v3 is deprecated. Go to Mathlib v4

Theorem finprod_mem_sUnion

Modification history

2022-03-14 05:19
src/algebra/big_operators/finprod.lean
docs(algebra/*): Add docstrings to additive lemmas (#12578) …
Modified finprod_mem_sUnionView on Github →
2021-12-13 17:35
src/algebra/big_operators/finprod.lean
refactor(data/set/pairwise): Make arguments of `set.pairwise` semi-implicit (#10740) …
Modified finprod_mem_sUnionView on Github →
2021-10-31 00:02
src/algebra/big_operators/finprod.lean
chore(data/set/pairwise): rename `set.pairwise_on` to `set.pairwise` to match `list.pairwise` and `multiset.pairwise` (#10035)
Modified finprod_mem_sUnionView on Github →
2021-04-22 20:22
src/algebra/big_operators/finprod.lean
refactor(algebra/big_operators/finprod) move finiteness assumptions to be final parameters (#7196) …
Modified finprod_mem_sUnionView on Github →
2021-04-07 02:18
src/algebra/big_operators/finprod.lean
feat(data/finsum): sums over sets and types with no finiteness hypotheses (#6355) …
Added finprod_mem_sUnionView on Github →