Fermat's last theorem for n=3

Stream: maths

[Riccardo Brasca]

@Ruben Van de Velde If I remember correctly you were working on the case n=3 of Fermat's last theorem. What is the status of your project? I think this case has to be treated by hand, even if 3 is a regular prime.

[Riccardo Brasca]

I found you repository, and

lemma flt_three
  {a b c : ℤ}
  (ha : a ≠ 0)
  (hb : b ≠ 0)
  (hc : c ≠ 0) :
  a ^ 3 + b ^ 3 ≠ c ^ 3

is sorry free! Congratulations! Are you interested in PRing this to mathlib?

[Ruben Van de Velde]

Yeah, next step is probably figuring out if there's anything I can split out or if I should just make a 2500 line PR. I haven't had much time for it recently

[Yaël Dillies]

Oh are you actually using docs#zsqrtd? It seems that this is a quite dated construct that either needs to be replaced by the more general machinery we now have or be substantially reworked to bring it up to today's standards.

[Riccardo Brasca]

docs#zsqrt is unfortunately mathematically wrong, in the sense that we should consider the ring of integers of $\mathbb{Q}(\sqrt{d})$.

[Riccardo Brasca]

It's surprisingly that it is enough for d=-3, but of course a proof is a proof

[Yaël Dillies]

Yeah so a first step would be to get rid of the use of zsqrtd in the proof.

[Riccardo Brasca]

We really need a number_theory/quadratic_field folder...

[Eric Rodriguez]

Imagine telling people that we have the discriminant of the p^nth cyclotomic field and not the rth quadratic field :D

[Ruben Van de Velde]

I have no particular interest in reworking the proof I have using the the ring of integers of $\mathbb{Q}(\sqrt{-3})$; if people think that's the way to go, we might need to find another volunteer :)

[Eric Wieser]

Sorry, docs#zsqrtd is wrong as in doesn't accurately model what it claims to, or just isn't what's needed here?

[Kevin Buzzard]

I think the issue is that mathematically the integers of $\mathbb{Q}(\sqrt{-3})$ is strictly bigger than $\mathbb{Z}[\sqrt{-3}]$ as it also contains $(1+\sqrt{-3})/2$.

[Eric Wieser]

Should we just change zsqrtd to sqrtd ℤ, making ℤ an argument?

[Riccardo Brasca]

It's "wrong" in the sense it's not mathematically interesting (at least, not always). For example what one wants is $\mathbb{Z}[\frac{1+\sqrt{-3}}{2}]$ as Kevin said

[Riccardo Brasca]

In any case what we probably want is a characteristic predicate saying that a field is a quadratic extension of $\mathbb{Q}$ associated to $d$, and then we abstractly have its ring of integers.

[Riccardo Brasca]

Something like "the dimension over $\mathbb{Q}$ is 2 and there is an element whose square is d, where d is a squarefree integer".

[Kevin Buzzard]

The ring zsqrt d is relevant for eg solutions to Pell's equation when d isn't squarefree; IIRC this is why Mario made that structure in the first place. I think it plays a useful role; we number theorists can develop the theory of integers of number fields elsewhere.

[Kevin Buzzard]

There's a theory of orders in number fields, they relate to ring class fields (or is it ray class fields, I can never remember which is which) and a theorem saying that most ideals factor uniquely into primes etc.

[Anne Baanen]

Eric Wieser said:

Should we just change zsqrtd to sqrtd ℤ, making ℤ an argument?

Alex, Nirvana, Sander and I are working on defining a "generic quadratic ring", i.e. R[X] / X^2 - aX - b for arbitrary rings R and a, b : R.

[Kevin Buzzard]

Oh that's a nice approach!