ready_for_mathlib

Stream: FLT-regular

[Riccardo Brasca]

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.

I for example added

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]

Riccardo Brasca said:

I for example added

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]

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

[Riccardo Brasca]

But I can read LaTeX :)

[Riccardo Brasca]

Thanks for the example. So let's add domain

[Riccardo Brasca]

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

[Riccardo Brasca]

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]

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

[Chris Birkbeck]

(deleted)

[Riccardo Brasca]

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

[Riccardo Brasca]

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.

I for example added

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]

Riccardo Brasca said:

I for example added

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]

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

[Riccardo Brasca]

But I can read LaTeX :)

[Riccardo Brasca]

Thanks for the example. So let's add domain

[Riccardo Brasca]

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

[Riccardo Brasca]

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]

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

[Chris Birkbeck]

(deleted)

[Riccardo Brasca]

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