feat(is_cyclotomic_extension/basic): add is_cyclotomic_extension.equiv

[riccardobrasca]

We add add is_cyclotomic_extension.equiv: being a cyclotomic extension is preserved by alg_equiv.

From flt-regular

---

[ericrbg]

Should we call this map? I was expecting this to be the fact that two n-th cyclotomic extensions were equivalent, which is something I don't think we actually yet have!

[riccardobrasca]

Should we call this map? I was expecting this to be the fact that two n-th cyclotomic extensions were equivalent, which is something I don't think we actually yet have!

This is to match names like module.finite.equiv. map seems inaccurate, since we really need an equiv.

Concerning the isomorphism, for S a singleton, it should be very easy to prove its existence, via is_cyclotomic_extension.splitting_field_X_pow_sub_one and polynomial.is_splitting_field.alg_equiv (taht suggest as name is_cyclotomic_extension.alg_equiv).

[riccardobrasca]

Should we call this map? I was expecting this to be the fact that two n-th cyclotomic extensions were equivalent, which is something I don't think we actually yet have!

This is to match names like module.finite.equiv. map seems inaccurate, since we really need an equiv.

Concerning the isomorphism, for S a singleton, it should be very easy to prove its existence, via is_cyclotomic_extension.splitting_field_X_pow_sub_one and polynomial.is_splitting_field.alg_equiv (taht suggest as name is_cyclotomic_extension.alg_equiv).

This turned out to be a one liner, so I added it.

[ericrbg]

oh, nice! do you know if it works in the general infinite case? if you don't, I may have a think about it for fun soon.

[riccardobrasca]

oh, nice! do you know if it works in the general infinite case? if you don't, I may have a think about it for fun soon.

We should first of all generalize it to any finite set (this shouldn't be hard by induction, we have all we need). Also, it should be true for any integral_domain, but this looks more difficult. I am pretty sure it's true also in the infinite case (for fields say, just to be sure), but I have to think a little to it.

[riccardobrasca]

I've added the lemmas needed to use trans to prove equiv, but unfortunately trans has additional assumptions (especially no_zero_smul_divisors B C, that is really needed) that are not needed for equiv. I think we can keep the new lemmas, that are in any case interesting, but also the current proof of equiv.

[riccardobrasca]

I've added the lemmas needed to use trans to prove equiv, but unfortunately trans has additional assumptions (especially no_zero_smul_divisors B C, that is really needed) that are not needed for equiv. I think we can keep the new lemmas, that are in any case interesting, but also the current proof of equiv.

I can maybe relax a little bit the assumptions in trans, let me try.

[riccardobrasca]

I've added the lemmas needed to use trans to prove equiv, but unfortunately trans has additional assumptions (especially no_zero_smul_divisors B C, that is really needed) that are not needed for equiv. I think we can keep the new lemmas, that are in any case interesting, but also the current proof of equiv.

I can maybe relax a little bit the assumptions in trans, let me try.

Much better now!

[bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests