Zulip Chat Archive

Stream: new members

Topic: product of integers


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)

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.

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.

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: Dec 20 2023 at 11:08 UTC