normal_iff_forall_map_eq — Mathlib

English

Normal F K iff for all AlgEquiv σ: L ≃ₐ[F] L, map (toAlgHom σ) K = K.

Русский

Normal F K эквивалентно тому, что для всех AlgEquiv σ: L ≃ₐ[F] L выполняется map (toAlgHom σ) K = K.

LaTeX

$$$\mathrm{Normal} F K \iff \forall \sigma : L \simeq_{F} L, K^{\sigma} = K$$$

Lean4

theorem normal_iff_forall_map_eq : Normal F K ↔ ∀ σ : L →ₐ[F] L, K.map σ = K :=
  ⟨fun h σ ↦ (K.fieldRange_val ▸ AlgHom.map_fieldRange K.val σ).trans (normal_iff_forall_fieldRange_eq.1 h _), fun h ↦
    normal_iff_forall_map_le.2 (fun σ ↦ (h σ).le)⟩

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