product with variable number of factors

Stream: maths

[Nicholas McConnell]

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]

finset.prod

[Nicholas McConnell]

Alright, thanks, I'll look into that

[Kevin Buzzard]

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]

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

Not what I'm asking...

[Nicholas McConnell]

But I'm willing to believe they relate.

[Reid Barton]

Are you sure? I think finset.product does that

[Nicholas McConnell]

"product" is an unknown identifier

[Reid Barton]

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

[Nicholas McConnell]

Oh, okay...

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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]

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

[Bryan Gin-ge Chen]

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

[Nicholas McConnell]

Alright, thanks Bryan

[Nicholas McConnell]

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]

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')