mathlib

0d14ee8b - feat(field_theory/finite/galois_field): Finite fields are Galois (#14290)

feat(field_theory/finite/galois_field): Finite fields are Galois (#14290) This PR also generalizes a section of `field_theory/finite/basic` from `[char_p K p]` to `[algebra (zmod p) K]`. This is indeed a generalization, due to the presence of the instance `zmod.algebra`.