## Stream: maths

### Topic: product with variable number of factors

#### Nicholas McConnell (Feb 20 2020 at 16:18):

To prove that if p is prime and p = 4k + 1, then -1 is a square modulo p.

I propose to use Wilson's Theorem, which states (p-1)! == -1 (mod p).

In Lean, what's the best way to tackle a product of a variable number of factors?

#### Kevin Buzzard (Feb 20 2020 at 16:19):

finset.prod

#### Nicholas McConnell (Feb 20 2020 at 16:19):

Alright, thanks, I'll look into that

#### Kevin Buzzard (Feb 20 2020 at 16:20):

Things like this are often more challenging than they look for beginners, but go for it and get stuck and ask here and people will be happy to help. This is a great little project.

#### Nicholas McConnell (Feb 29 2020 at 23:33):

I just imported finset today, and apparently, finset.prod actually takes the Cartesian product of two sets

#### Nicholas McConnell (Feb 29 2020 at 23:35):

But I'm willing to believe they relate.

#### Reid Barton (Feb 29 2020 at 23:35):

Are you sure? I think finset.product does that

#### Nicholas McConnell (Feb 29 2020 at 23:35):

"product" is an unknown identifier

#### Reid Barton (Feb 29 2020 at 23:36):

I'm doubly confused now, but finset.prod is in algebra.big_operators.

Oh, okay...

#### Kevin Buzzard (Feb 29 2020 at 23:38):

Another confusing thing about finset.prod is that it doesn't take the product of the elements of the finset, it also takes a map from the underlying type to a comm_monoid and takes the product of the images. In particular you can have repeated factors in your product.

#### Kevin Buzzard (Feb 29 2020 at 23:39):

Another confusing thing about it is that there's also finset.sum but it's hard to find the definition, because it's generated automatically by the @[to_additive] tag on finset.prod.

#### Kevin Buzzard (Feb 29 2020 at 23:42):

#eval finset.prod (finset.range 3) (λ n, n^2+1) -- 1*2*5=10

#### Kevin Buzzard (Feb 29 2020 at 23:46):

It might be worth adding that factorials are already in mathlib (as is the fact that -1 is a square mod p iff p isn't 3 mod 4, and probably Wilson's theorem too, but this definitely shouldn't stop you trying them yourself)

#### Nicholas McConnell (Feb 29 2020 at 23:57):

Out of curiosity, where are factorials and -1 being a square mod p in mathlib?

#### Bryan Gin-ge Chen (Mar 01 2020 at 00:03):

Here are factorials (I searched for "factorial"). The other fact that Kevin mentioned is here.

#### Nicholas McConnell (Mar 01 2020 at 00:06):

Alright, thanks Bryan

#### Nicholas McConnell (Mar 01 2020 at 18:55):

I'm just going to use the builtin ones now because my file is already really big and I have little time left to complete the project.

When I imported data.zmod.quadratic_reciprocity, the file broke down with 1000 problems, and they even persisted when I deleted that import and made the file have the same text it started with, until I restarted VSC. Is that supposedly the wrong import?

#### Bryan Gin-ge Chen (Mar 01 2020 at 19:11):

I don't think it's the wrong import, but I can't reproduce your issue either. Sometimes things like this happen if Lean runs out of memory. If it goes away after you restart Lean, I wouldn't worry too much about it. (Note that you can restart Lean without starting VS Code by hitting ctrl+shift+p and typing 'Lean: restart')

Last updated: May 14 2021 at 20:13 UTC