Zulip Chat Archive

Stream: maths

Topic: product with variable number of factors


view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Feb 20 2020 at 16:19):

finset.prod

view this post on Zulip Nicholas McConnell (Feb 20 2020 at 16:19):

Alright, thanks, I'll look into that

view this post on Zulip 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.

view this post on Zulip 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

Not what I'm asking...

view this post on Zulip Nicholas McConnell (Feb 29 2020 at 23:35):

But I'm willing to believe they relate.

view this post on Zulip Reid Barton (Feb 29 2020 at 23:35):

Are you sure? I think finset.product does that

view this post on Zulip Nicholas McConnell (Feb 29 2020 at 23:35):

"product" is an unknown identifier

view this post on Zulip Reid Barton (Feb 29 2020 at 23:36):

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

view this post on Zulip Nicholas McConnell (Feb 29 2020 at 23:36):

Oh, okay...

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Feb 29 2020 at 23:42):

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

view this post on Zulip 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)

view this post on Zulip Nicholas McConnell (Feb 29 2020 at 23:57):

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

view this post on Zulip 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.

view this post on Zulip Nicholas McConnell (Mar 01 2020 at 00:06):

Alright, thanks Bryan

view this post on Zulip 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?

view this post on Zulip 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