exists_linearIndependent_algEquiv_apply

English

There exists an element x in L such that the orbit { σ(x) | σ ∈ Aut_K(L) } is a basis of L over K.

Русский

Существует элемент x ∈ L, чья орбита под действием Галуа-автоморфизмов образует базис L над K.

LaTeX

$$∃ x ∈ L : LinearIndependent_K ( (σ : L ≃ₐ[K] L) ↦ σ x )$$

Lean4

theorem exists_linearIndependent_algEquiv_apply : ∃ x : L, LinearIndependent K fun σ : L ≃ₐ[K] L ↦ σ x :=
  by
  obtain h | h := finite_or_infinite K
  · have := Module.finite_of_finite K (M := L)
    exact exists_linearIndependent_algEquiv_apply_of_finite K L
  · exact exists_linearIndependent_algEquiv_apply_of_infinite K L

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