krullTopology_discreteTopology_of_finiteDimensional

English

If L/K is finite-dimensional, the Krull topology on the K-automorphism group Aut_K(L) is discrete.

Русский

Если L/K имеет конечную размерность, то Крульова топология на Aut_K(L) дискретна.

LaTeX

$$$\\DiscreteTopology(\\mathrm{Aut}_K(L)).$$$

Lean4

instance krullTopology_discreteTopology_of_finiteDimensional (K L : Type*) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] : DiscreteTopology (L ≃ₐ[K] L) :=
  by
  rw [discreteTopology_iff_isOpen_singleton_one]
  change IsOpen ((⊥ : Subgroup (L ≃ₐ[K] L)) : Set (L ≃ₐ[K] L))
  rw [← IntermediateField.fixingSubgroup_top]
  exact IntermediateField.fixingSubgroup_isOpen ⊤

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