Zulip Chat Archive

Stream: new members

Topic: product of integers


view this post on Zulip rory (Nov 07 2019 at 14:09):

I'm trying to describe the product of a bunch of coprime integers. Since I want to describe finite integers, so I choose list nat. The way I find to write the product is list.foldr (*) 1 [2,3,5..], using a random list as an example. Is this the best way of doing this? (sorry for asking so much noob questions recently)

view this post on Zulip Anne Baanen (Nov 07 2019 at 16:41):

I'm trying to describe the product of a bunch of coprime integers. Since I want to describe finite integers, so I choose list nat. The way I find to write the product is list.foldr (*) 1 [2,3,5..], using a random list as an example. Is this the best way of doing this? (sorry for asking so much noob questions recently)

If you import algebra.big_operators, you get access to list.prod.

view this post on Zulip Chris Hughes (Nov 07 2019 at 16:44):

It's probably better to use finset.prod. Most of the useful lemmas are about finset.prod.

view this post on Zulip Bryan Gin-ge Chen (Nov 07 2019 at 16:52):

Out of curiosity is there a reason (other than historical accident) why the lemmas about sums and products are mostly at the finset level rather than list? Are finsets intrinsically more well-suited for summing (or proving things about sums) than lists?


Last updated: May 08 2021 at 19:11 UTC