Theorem 11.6

Stream: FLT

[Abhijit Mudigonda]

Hi! I'm a grad student participating in the ongoing Simons workshop. I do some work with quaternionic automorphic forms in my regular work so I figured I'd take a stab at 11.6, using Fujisaki as a black box for now (though it seems like it's close to being done). Is anyone already working on 11.6? I don't see it on the dashboard, at least.

[Kevin Buzzard]

yeah go for it! I was working on trying to write down exactly what we needed to prove this but right now I haven't even got around to making issues with some of the sorries and this is one of them. Feel free to make a PR!

[Abhijit Mudigonda]

I'm sure you already got a ping for it, but here's the PR. I'm pretty new to Lean stuff, so let me know if there are things that I should fix.

[Alex Kontorovich]

Great work Abhijit!

[Kevin Buzzard]

Oh I've not looked at GitHub notifications since before Cambridge, thanks for the heads up!