Are there theorems about prime fields in Mathlib4?

Stream: mathlib4

[aprilgrimoire]

Hi! It is a basic result that the minimal subfield of any field is either isomorphic to Q or F_p. Are there theorems in mathlib4 expressing this fact and I'm incapable of finding them, or they aren't added yet?
Thanks.

[David Loeffler]

There is docs#DivisionRing.toRatAlgebra, stating that any characteristic 0 division ring is an algebra over Q, and docs#ZMod.algebra which is the analogue for characteristic p. This isn't quite what you asked for, but hopefully it's a step in the right direction.

[Adam Topaz]

We should have a prop-valued class called IsPrimeField F for a type F satisfying [Field F]. I introduced such a class in a personal Lean(3) project, but never moved it over to mathlib. And yes, we should have a function called primeSubfield F for a type F with a field instance which gives the prime subfield as a docs#Subfield .

[Adam Topaz]

If Subfield has a Bot instance, that could be used as well.

[Adam Topaz]

Here is the lean3 definition I had in that project, in case it helps: https://github.com/adamtopaz/lean-acl-pairs/blob/dcf56cdcfd8f2b1fcc822ae1012057d881e77eee/src/bridge.lean#L14