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.

instance Subfield.charP {F : Type u_1} [Field F] (L : Subfield F) (p : ℕ) [CharP F p] : CharP (↥L) p

instance Subfield.expChar {F : Type u_1} [Field F] (L : Subfield F) (p : ℕ) [ExpChar F p] : ExpChar (↥L) p

instance IntermediateField.charZero {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] (L : IntermediateField F E) [CharZero F] : CharZero ↥L

instance IntermediateField.charP {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] (L : IntermediateField F E) (p : ℕ) [CharP F p] : CharP (↥L) p

instance IntermediateField.expChar {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] (L : IntermediateField F E) (p : ℕ) [ExpChar F p] : ExpChar (↥L) p

instance IntermediateField.charP' {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] (L : IntermediateField F E) (p : ℕ) [CharP E p] : CharP (↥L) p

instance IntermediateField.expChar' {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] (L : IntermediateField F E) (p : ℕ) [ExpChar E p] : ExpChar (↥L) p