mapPowExpCharPowOfIsSeparable — Mathlib

English

If E/F is separable with q, then the image of a basis under raising to q^n is a basis.

Русский

Если E/F разделяемо с q, то образ базиса под возведением в q^n — базис.

LaTeX

$$$\text{Basis} \to \text{Basis}$$$

Lean4

/-- If `E / F` is a separable extension of exponential characteristic `q`, if `{ u_i }` is an
`F`-basis of `E`, then `{ u_i ^ (q ^ n) }` is also an `F`-basis of `E`
for any natural number `n`. -/
def mapPowExpCharPowOfIsSeparable [Algebra.IsSeparable F E] (b : Basis ι F E) : Basis ι F E :=
  .mk (b.linearIndependent.map_pow_expChar_pow_of_isSeparable q n)
    (Field.span_map_pow_expChar_pow_eq_top_of_isSeparable q n b.span_eq).ge

Похожие утверждения