EtaleFundamentalGroups.exists_uniform_purelyInseparable_exponent
A single Frobenius power sends every element of a finite purely inseparable extension into the original field.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped BigOperators
universe u
namespace EtaleFundamentalGroups
variable (k L : Type u) [Field k] [Field L] [Algebra k L]
variable [IsPurelyInseparable k L] [FiniteDimensional k L]
variable (p : ℕ) [ExpChar k p] [ExpChar L p]Lean source · statement
theorem exists_uniform_purelyInseparable_exponent :
∃ n : ℕ, ∀ x : L, x ^ p ^ n ∈ (algebraMap k L).range