mem_bot_iff_fixed — Mathlib

English

An element x of E lies in the bottom intermediate field iff every automorphism in Gal(E/F) fixes x.

Русский

Элемент x ∈ E принадлежит нижнему промежуточному полю тогда и только тогда, когда каждый автоморфизм в Gal(E/F) фиксирует x.

LaTeX

$$$x\in (\bot) \iff \forall f: E\simeq_F E, f(x)=x$$$

Lean4

theorem mem_bot_iff_fixed [IsGalois F E] [FiniteDimensional F E] (x : E) :
    x ∈ (⊥ : IntermediateField F E) ↔ ∀ f : E ≃ₐ[F] E, f x = x :=
  by
  rw [← fixedField_top, mem_fixedField_iff]
  simp only [Subgroup.mem_top, forall_const]

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