mem_galBasis_iff — Mathlib

English

A subset of L ≃_K L is in galBasis iff it is the carrier of Gal(L/E) for some finite E/K.

Русский

Подмножество Gal(L/K) принадлежит galBasis тогда и только тогда, когда является каркаc-носителем Gal(L/E) для некоторого конечного E/K.

LaTeX

$$$U \\in galBasis(K,L) \\iff U \\in (\\{ g.carrier : g \\in Gal(L/E)\\})_{E: finiteK L}$$$

Lean4

/-- A subset of `L ≃ₐ[K] L` is a member of `galBasis K L` if and only if it is the underlying set
of `Gal(L/E)` for some finite subextension `E/K`. -/
theorem mem_galBasis_iff (K L : Type*) [Field K] [Field L] [Algebra K L] (U : Set (L ≃ₐ[K] L)) :
    U ∈ galBasis K L ↔ U ∈ (fun g => g.carrier) '' fixedByFinite K L :=
  Iff.rfl

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