normalBasis — Mathlib

English

The normalBasis K L is a basis of L over K indexed by Aut_K(L).

Русский

normalBasis K L — это базис L над K индексированный по Aut_K(L).

LaTeX

$$normalBasis : Module.Basis (AlgEquiv K L L) K L$$

Lean4

/-- Given a finite Galois extension `L/K`, `normalBasis K L` is a basis of `L` over `K`
that is an orbit under the Galois group action. -/
noncomputable def normalBasis : Module.Basis (L ≃ₐ[K] L) K L :=
  basisOfLinearIndependentOfCardEqFinrank (exists_linearIndependent_algEquiv_apply K L).choose_spec
    (Fintype.card_eq_nat_card.trans <| card_aut_eq_finrank K L)

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