krullTopology — Mathlib

English

For a field extension L/K, krullTopology defines a topological space structure on Aut_K(L) using the galGroupBasis.

Русский

Для расширения L/K крауловая топология задаёт топологическое пространство на Aut_K(L) через galGroupBasis.

LaTeX

$$$krullTopology(K,L) := Topology(Aut_K(L), galGroupBasis(K,L))$$$

Lean4

/-- For a field extension `L/K`, `krullTopology K L` is the topological space structure on
`L ≃ₐ[K] L` induced by the group filter basis `galGroupBasis K L`. -/
instance krullTopology (K L : Type*) [Field K] [Field L] [Algebra K L] : TopologicalSpace (L ≃ₐ[K] L) :=
  GroupFilterBasis.topology (galGroupBasis K L)

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