Completion of FLT-regular

Stream: FLT-regular

[Riccardo Brasca]

Let's use this topic to discuss future work or whatever.

[Riccardo Brasca]

@Xavier Roblot How far are from using Minkowski's bound to prove that $\mathbb{Q}(\zeta_5)$ is a PID? The bound is 1...

[Riccardo Brasca]

It seems that $\mathbb{Q}(\zeta_p)$ is norm euclidean for $p = 3, 5, 7, 11$, so maybe it is not completely impossible to prove that $p$ is regular in these cases.

(It is euclidean also if $p = 17, 19$ but I don't know if it is norm euclidean, and this is the complete list of primes such that is $\mathbb{Q}(\zeta_p)$ is a PID).

[Johan Commelin]

Huge congrats to all people involved!

[Xavier Roblot]

Riccardo Brasca said:

Xavier Roblot How far are from using Minkowski's bound to prove that $\mathbb{Q}(\zeta_5)$ is a PID? The bound is 1...

I'm still fighting with the proof of Hermite's theorem at the moment but adapting the existing results in CanonicalEmbedding to deduce the classical bound on the norm of ideals in ideal classes is next on my list. This would be enough to deduce that $\mathbb{Q}(\zeta_5)$ is principal. I am not sure about the other ones though (I'll have to do the computations when I have time).

[Xavier Roblot]

(I am in class now :grinning_face_with_smiling_eyes: )

[Riccardo Brasca]

For $p=7$ it is 8. Anyway getting $3$ and $5$ is already interesting.

[Xavier Roblot]

Well, we can still prove that all integral ideals of norm $\le 8$ are principal