Cyclotomic extensions of finite fields are finite

Stream: Is there code for X?

[Michael Stoll]

I'm missing an instance that says that cyclotomic_field n F is finite if F is a finite field.
@Riccardo Brasca Is this something that could be included in #14463?

[Michael Stoll]

Or maybe, this should work via: cyclotomic_field n F is a finite(-dimensional) extension of F; a finite extension of a finite field is finite.

[Riccardo Brasca]

Yes, that will work immediately. I have some draft code (I will open a PR maybe tomorrow) to show that cyclotomic_field n F is always a cyclotomic extension of F (I mean, even if n = 0 in F, it isn't a n-th cyclotomic extension but a m-th one, where n = p^k * m where p = char(F)), so this will work in general.

[Riccardo Brasca]

Note that cyclotomic_field n F is just (cyclotomic n K).splitting_field, so you can already use all the API for splitting_field.

[Riccardo Brasca]

Maybe docs#finite_dimensional.fintype_of_fintype already works (but it cannot be an instance)

[Riccardo Brasca]

In general all the theorems saying that L is finite because K satisfies some condition and L is related to K, cannot be instances, since Lean cannot guess K.

[Michael Stoll]

OK. So this appears to work:

  let FF := cyclotomic_field 8 F,
  haveI : finite_dimensional F FF := polynomial.is_splitting_field.finite_dimensional _ _,
  haveI : fintype FF := finite_dimensional.fintype_of_fintype F FF,

Thanks!

[Riccardo Brasca]

Do you need the first haveI?

[Michael Stoll]

Yes; otherwise the second haveI complains.

[Riccardo Brasca]

Mmh, this makes me thinking that maybe cyclotomic_field should be just an abbreviation rather than a def, so Lean can automatically use all the instances for splitting_field

[Riccardo Brasca]

I will see after #14463 gets merged

[Eric Rodriguez]

Can't we just @derive it?

[Riccardo Brasca]

Sure, but we have to do it for all the instance splitting_field has, right?