## Stream: FLT-regular

### Topic: Completion of FLT-regular

#### Riccardo Brasca (Dec 05 2023 at 12:57):

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

#### Riccardo Brasca (Dec 05 2023 at 13:06):

@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 (Dec 05 2023 at 13:38):

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 (Dec 05 2023 at 14:30):

Huge congrats to all people involved!

#### Xavier Roblot (Dec 05 2023 at 14:42):

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 (Dec 05 2023 at 14:42):

(I am in class now :grinning_face_with_smiling_eyes: )

#### Riccardo Brasca (Dec 05 2023 at 14:46):

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

#### Xavier Roblot (Dec 05 2023 at 14:49):

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

Last updated: Dec 20 2023 at 11:08 UTC