fixedField_top — Mathlib

English

If the ambient extension is IsGalois and finite dimensional, then fixedField of the top subgroup equals bottom field.

Русский

Если расширение изолировано как IsGalois и конечномерно, то фиксированное поле верхней подгруппы равно нижнему полю.

LaTeX

$$[IsGalois F E] [FiniteDimensional F E] ⇒ fixedField(⊤) = ⊥$$

Lean4

@[simp]
theorem fixedField_top [IsGalois F E] [FiniteDimensional F E] : fixedField (⊤ : Subgroup (E ≃ₐ[F] E)) = ⊥ := by
  rw [← fixingSubgroup_bot, fixedField_fixingSubgroup]

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