instIsTopologicalGroupAlgEquiv — Mathlib

English

Krull topology makes AlgEquiv K L L a topological group.

Русский

Круллова топология делает AlgEquiv(K,L,L) топологической группой.

LaTeX

$$$IsTopologicalGroup\\ (Aut_K(L))$ with Krull topology$$

Lean4

/-- For a field extension `L/K`, the Krull topology on `L ≃ₐ[K] L` makes it a topological group. -/
@[stacks 0BMJ "We define Krull topology directly without proving the universal property"]
instance (K L : Type*) [Field K] [Field L] [Algebra K L] : IsTopologicalGroup (L ≃ₐ[K] L) :=
  GroupFilterBasis.isTopologicalGroup (galGroupBasis K L)

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