## Stream: FLT-regular

#### Riccardo Brasca (Oct 29 2021 at 10:28):

I've addd a folder ready_for_mathlib where we can add lemmas whose statement is in a PR ready status. So there can be sorried lemmas, but once proved one can PR them. Feel free to create new files and move results there.

lemma is_root_cyclotomic_iff {n : ℕ} {R : Type*} [comm_ring R] {μ : R}
: is_primitive_root μ n ↔ is_root (cyclotomic n R) μ := sorry


I am not even sure it is true in this generality, no problem if we need to add assumptions, but let's try to be as general as possible.

#### Antoine Chambert-Loir (Oct 29 2021 at 13:43):

Riccardo Brasca said:

lemma is_root_cyclotomic_iff {n : ℕ} {R : Type*} [comm_ring R] {μ : R}
: is_primitive_root μ n ↔ is_root (cyclotomic n R) μ := sorry


I am not even sure it is true in this generality, no problem if we need to add assumptions, but let's try to be as general as possible.

I fear it isn't. Take $R=\mathbf F_2[\epsilon]$ ($\epsilon^2=0$), with $\mu=1+\eps$. Then $\mu\neq \pm1 =1$, but $\mu^2=1$. Probably, either $n$ invertible, or $R$ an integral domain, more generally, $n$ regular, will be enough.

#### Riccardo Brasca (Oct 29 2021 at 13:45):

For some reasons you have to use a double dollar sign in Zulip

#### Riccardo Brasca (Oct 29 2021 at 13:45):

But I can read LaTeX :)

#### Riccardo Brasca (Oct 29 2021 at 13:47):

Thanks for the example. So let's add domain

#### Riccardo Brasca (Oct 29 2021 at 13:48):

Ah sure, the reason is simply that there are more roots than the degree!

#### Riccardo Brasca (Nov 03 2021 at 09:41):

I've created a wiki with the list of files in the ready_for_mathlib folder, so we can keep track of who PR what.

Don't hesitate to put the results you need there , even if they are sorried, if you think the statement is suitable for mathlib.

#### Alex J. Best (Nov 03 2021 at 09:54):

Sorry I've been a little disorganized with PRing things so far, but everything I did should have flt-regular as a searchable string in the mathlib pull request body

(deleted)

#### Riccardo Brasca (Nov 03 2021 at 09:56):

No problem for that! It's just to avoid to open two PR for the same stuff.

#### Riccardo Brasca (Oct 29 2021 at 10:28):

I've addd a folder ready_for_mathlib where we can add lemmas whose statement is in a PR ready status. So there can be sorried lemmas, but once proved one can PR them. Feel free to create new files and move results there.

lemma is_root_cyclotomic_iff {n : ℕ} {R : Type*} [comm_ring R] {μ : R}
: is_primitive_root μ n ↔ is_root (cyclotomic n R) μ := sorry


I am not even sure it is true in this generality, no problem if we need to add assumptions, but let's try to be as general as possible.

#### Antoine Chambert-Loir (Oct 29 2021 at 13:43):

Riccardo Brasca said:

lemma is_root_cyclotomic_iff {n : ℕ} {R : Type*} [comm_ring R] {μ : R}
: is_primitive_root μ n ↔ is_root (cyclotomic n R) μ := sorry


I am not even sure it is true in this generality, no problem if we need to add assumptions, but let's try to be as general as possible.

I fear it isn't. Take $R=\mathbf F_2[\epsilon]$ ($\epsilon^2=0$), with $\mu=1+\eps$. Then $\mu\neq \pm1 =1$, but $\mu^2=1$. Probably, either $n$ invertible, or $R$ an integral domain, more generally, $n$ regular, will be enough.

#### Riccardo Brasca (Oct 29 2021 at 13:45):

For some reasons you have to use a double dollar sign in Zulip

#### Riccardo Brasca (Oct 29 2021 at 13:45):

But I can read LaTeX :)

#### Riccardo Brasca (Oct 29 2021 at 13:47):

Thanks for the example. So let's add domain

#### Riccardo Brasca (Oct 29 2021 at 13:48):

Ah sure, the reason is simply that there are more roots than the degree!

#### Riccardo Brasca (Nov 03 2021 at 09:41):

I've created a wiki with the list of files in the ready_for_mathlib folder, so we can keep track of who PR what.

Don't hesitate to put the results you need there , even if they are sorried, if you think the statement is suitable for mathlib.

#### Alex J. Best (Nov 03 2021 at 09:54):

Sorry I've been a little disorganized with PRing things so far, but everything I did should have flt-regular as a searchable string in the mathlib pull request body

(deleted)

#### Riccardo Brasca (Nov 03 2021 at 09:56):

No problem for that! It's just to avoid to open two PR for the same stuff.

Last updated: Dec 20 2023 at 11:08 UTC