Documentation

Mathlib.Algebra.CharP.IntermediateField

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.

source
instance Subfield.charP {F : Type u_1} [Field F] (L : Subfield F) (p : ℕ) [CharP F p] :
CharP (↥L) p
Equations
  • ⋯ = ⋯
source
instance Subfield.expChar {F : Type u_1} [Field F] (L : Subfield F) (p : ℕ) [ExpChar F p] :
ExpChar (↥L) p
Equations
  • ⋯ = ⋯
source
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
Equations
  • ⋯ = ⋯
source
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
Equations
  • ⋯ = ⋯
source
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
Equations
  • ⋯ = ⋯
source
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
Equations
  • ⋯ = ⋯
source
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
Equations
  • ⋯ = ⋯