fixedField_bot — Mathlib

English

In an infinite Galois setting, the fixed field of the top subgroup equals the bottom field.

Русский

В бесконечной Галуа-теории фиксированное поле верхней подгруппы равно нижнему полю.

LaTeX

$$$ \text{fixedField}(\top) = \bot $$$

Lean4

theorem fixedField_bot [IsGalois k K] : IntermediateField.fixedField (⊤ : Subgroup (K ≃ₐ[k] K)) = ⊥ := by
  rw [← IntermediateField.fixingSubgroup_bot, fixedField_fixingSubgroup]

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