krullTopology_isTotallySeparated — Mathlib

English

For an algebraic extension L/K, the set of all K-automorphisms of L is totally separated in the Krull topology.

Русский

Для алгебраического расширения L/K множество всех K-автоморфизмов L полностью разделено в топологии Круль.

LaTeX

$$$\\text{IsTotallySeparated}(\\mathrm{Aut}_K(L)).$$$

Lean4

/-- If `L/K` is an algebraic field extension, then the Krull topology on `L ≃ₐ[K] L` is
  totally disconnected. -/
theorem krullTopology_isTotallySeparated {K L : Type*} [Field K] [Field L] [Algebra K L] [Algebra.IsIntegral K L] :
    IsTotallySeparated (Set.univ : Set (L ≃ₐ[K] L)) :=
  (totallySeparatedSpace_iff _).mp inferInstance

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