product of integers

Stream: new members

[rory]

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]

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]

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

[Bryan Gin-ge Chen]

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?