feat(FieldTheory/KrullTopology): stabilizers are open for the Krull topology (leanprover-community#34885)

`stabilizer_isOpen_of_isIntegral`: For an algebraic field extension `L/K`, the stabilizer in `Gal(L/K)` of any element in `L` is open for the Krull topology.

Also fix typo in docstrings for `krullTopology_isTotallySeparated`.

Co-authored-by: bwangpj <70694994+bwangpj@users.noreply.github.com>

Author: bwangpj

Mathlib/FieldTheory/KrullTopology.lean

@@ -38,8 +38,11 @@ all intermediate fields `E` with `E/K` finite dimensional.
 - `krullTopology_t2 K L`. For an integral field extension `L/K`, the topology `krullTopology K L`
   is Hausdorff.
 
-- `krullTopology_totallyDisconnected K L`. For an integral field extension `L/K`, the topology
-  `krullTopology K L` is totally disconnected.
+- `krullTopology_isTotallySeparated K L`. For an integral field extension `L/K`, the topology
+  `krullTopology K L` is totally separated.
+
+- `stabilizer_isOpen_of_isIntegral`: For an integral field extension `L/K`, the stabilizer
+  in `Gal(L/K)` of any element in `L` is open for the Krull topology.
 
 - `IntermediateField.finrank_eq_fixingSubgroup_index`: given a Galois extension `K/k` and an
   intermediate field `L`, the `[L : k]` as a natural number is equal to the index of the
@@ -237,7 +240,7 @@ instance {K L : Type*} [Field K] [Field L] [Algebra K L] [Algebra.IsIntegral K L
   exact ⟨x, IntermediateField.mem_adjoin_simple_self K x, hx⟩
 
 /-- If `L/K` is an algebraic field extension, then the Krull topology on `Gal(L/K)` is
-  totally disconnected. -/
+  totally separated. -/
 theorem krullTopology_isTotallySeparated {K L : Type*} [Field K] [Field L] [Algebra K L]
     [Algebra.IsIntegral K L] : IsTotallySeparated (Set.univ : Set Gal(L/K)) :=
   (totallySeparatedSpace_iff _).mp inferInstance
@@ -251,6 +254,23 @@ instance krullTopology_discreteTopology_of_finiteDimensional (K L : Type*) [Fiel
   rw [← IntermediateField.fixingSubgroup_top]
   exact IntermediateField.fixingSubgroup_isOpen ⊤
 
+section MulAction
+
+variable {K L : Type*} [Field K] [Field L] [Algebra K L]
+
+/-- If `L/K` is an algebraic field extension, then the stabilizer
+in `Gal(L/K)` of any element in `L` is open for the Krull topology. -/
+theorem stabilizer_isOpen_of_isIntegral [Algebra.IsIntegral K L] (x : L) :
+    IsOpen (MulAction.stabilizer Gal(L/K) x : Set Gal(L/K)) := by
+  open IntermediateField in
+  let E := adjoin K {x}
+  have hL : FiniteDimensional K E := adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral x)
+  convert fixingSubgroup_isOpen E
+  ext g
+  simpa using (forall_mem_adjoin_smul_eq_self_iff K (S := {x}) g).symm
+
+end MulAction
+
 namespace IntermediateField
 
 variable {k E : Type*} (K : Type*) [Field k] [Field E] [Field K]