Zulip Chat Archive

Stream: FLT

Topic: FLT3

Riccardo Brasca (Jul 11 2024 at 16:49):

#14653 finishes the proof of flt3.

David Michael Roberts (Jul 12 2024 at 02:10):

Maybe I'm being silly, but should I dig into the references to find out what λ is at https://github.com/leanprover-community/mathlib4/blob/378a3ffa7fd71b6cac27d8c30d13faf1e76e2adc/Mathlib/NumberTheory/FLT/Three.lean#L30 ?

David Michael Roberts (Jul 12 2024 at 02:11):

Is it purely the thing defined further down (i.e. ζ₃ - 1)? I'd suggest reordering to put the definition first.

Riccardo Brasca (Jul 12 2024 at 08:01):

Yes, I thought I had already added it, but it seems I didn't. Thanks!

Ruben Van de Velde (Jul 16 2024 at 09:55):

FLT#113

Last updated: May 02 2025 at 03:31 UTC