# 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: May 08 2021 at 19:11 UTC