Theorems · Theorem · field theory

Field.span_map_pow_expChar_pow_eq_top_of_isSeparable

∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (q n : ℕ) [hF : ExpChar F q]
  {ι : Type u_1} {v : ι → E} [Algebra.IsSeparable F E],
  Submodule.span F (Set.range v) = ⊤ → Submodule.span F (Set.range fun x => v x ^ q ^ n) = ⊤

If E / F is a separable extension of exponential characteristic q, if { u_i } is a family of elements of E which F-linearly spans E, then { u_i ^ (q ^ n) } also F-linearly spans E for any natural number n.

Defined in

Mathlib.FieldTheory.PurelyInseparable.PerfectClosure

Cited by

0 results in Mathlib

Foundations

Depth 198 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldFieldAlgebraExpCharAlgebra.IsSeparable