top_fixedByFinite — Mathlib

English

The top subgroup is in fixedByFinite: Gal(L/K) belongs to fixedByFinite K L.

Русский

Гал(L/K) находится в fixedByFinite K L.

LaTeX

$$$\\top\\in fixedByFinite(K,L)$$$

Lean4

/-- If `L/K` is a field extension, then we have `Gal(L/K) ∈ fixedByFinite K L`. -/
theorem top_fixedByFinite {K L : Type*} [Field K] [Field L] [Algebra K L] : ⊤ ∈ fixedByFinite K L :=
  ⟨⊥, IntermediateField.instFiniteSubtypeMemBot K, IntermediateField.fixingSubgroup_bot⟩

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