mem_range_algebraMap_iff_fixed — Mathlib

English

An element x lies in the range of the algebra map F→E iff x is fixed by all E-automorphisms over F.

Русский

Элемент x лежит в образе алгебраического отображения F→E тогда и только тогда, когда каждый автоморфизм E над F фиксирует x.

LaTeX

$$$x\in \operatorname{range}(\text{algebraMap } F E) \iff \forall f: E\simeq_F E, f(x)=x$$$

Lean4

theorem mem_range_algebraMap_iff_fixed [IsGalois F E] [FiniteDimensional F E] (x : E) :
    x ∈ Set.range (algebraMap F E) ↔ ∀ f : E ≃ₐ[F] E, f x = x :=
  mem_bot_iff_fixed x

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