feat(Algebra/CharP/IntermediateField): characteristic of intermediate…

… fields (leanprover-community#10839)

Add some convenient instances for determining the characteristic of intermediate fields, similar to `SubsemiringClass.instCharZero`.

Mathlib.lean

@@ -101,6 +101,7 @@ import Mathlib.Algebra.CharP.Algebra
 import Mathlib.Algebra.CharP.Basic
 import Mathlib.Algebra.CharP.CharAndCard
 import Mathlib.Algebra.CharP.ExpChar
+import Mathlib.Algebra.CharP.IntermediateField
 import Mathlib.Algebra.CharP.Invertible
 import Mathlib.Algebra.CharP.LocalRing
 import Mathlib.Algebra.CharP.MixedCharZero

Mathlib/Algebra/CharP/IntermediateField.lean

@@ -0,0 +1,48 @@
+/-
+Copyright (c) 2024 Jz Pan. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jz Pan
+-/
+import Mathlib.FieldTheory.IntermediateField
+import Mathlib.Algebra.CharP.ExpChar
+
+/-!
+
+# Characteristic of intermediate fields
+
+This file contains some convenient instances for determining the characteristic of
+intermediate fields. Some char zero instances are not provided, since they are already
+covered by `SubsemiringClass.instCharZero`.
+
+-/
+
+variable {F E : Type*} [Field F] [Field E] [Algebra F E]
+
+namespace Subfield
+
+variable (L : Subfield F) (p : ℕ)
+
+instance charP [CharP F p] : CharP L p := RingHom.charP _ (algebraMap _ F).injective p
+
+instance expChar [ExpChar F p] : ExpChar L p := RingHom.expChar _ (algebraMap _ F).injective p
+
+end Subfield
+
+namespace IntermediateField
+
+variable (L : IntermediateField F E) (p : ℕ)
+
+instance charZero [CharZero F] : CharZero L :=
+  charZero_of_injective_algebraMap (algebraMap F _).injective
+
+instance charP [CharP F p] : CharP L p :=
+  charP_of_injective_algebraMap (algebraMap F _).injective p
+
+instance expChar [ExpChar F p] : ExpChar L p :=
+  expChar_of_injective_algebraMap (algebraMap F _).injective p
+
+instance charP' [CharP E p] : CharP L p := Subfield.charP L.toSubfield p
+
+instance expChar' [ExpChar E p] : ExpChar L p := Subfield.expChar L.toSubfield p
+
+end IntermediateField