Commit 2023-01-20 10:26 8176e5d6

View on Github →

feat: port Algebra.BigOperators.Pi (#1687)

Estimated changes

added theorem Finset.prod_apply
added theorem Finset.prod_fn
added theorem Finset.univ_sum_single
added theorem Fintype.prod_apply
added theorem Pi.list_prod_apply
added theorem Pi.multiset_prod_apply
added theorem Prod.fst_prod
added theorem Prod.snd_prod
added theorem RingHom.functions_ext
added theorem prod_mk_prod