fixedPoints_eq_bot — Mathlib

English

In a Galois group action, the fixed points subfield coincides with the bottom field.

Русский

При действии группы Галуа фиксированное подполе совпадает с нижним полем.

LaTeX

$$$ FixedPoints.intermediateField G = \bot $$$

Lean4

theorem fixedPoints_eq_bot [IsGaloisGroup G K L] : FixedPoints.intermediateField G = (⊥ : IntermediateField K L) :=
  by
  rw [eq_bot_iff]
  exact Algebra.IsInvariant.isInvariant

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