doc(FieldTheory/SeparableDegree): fix the formula in docstring (#9318)

Mathlib/FieldTheory/SeparableDegree.lean

@@ -25,9 +25,10 @@ This file contains basics about the separable degree of a field extension.
 
   **Remark:** if `E / F` is not algebraic, then this definition makes no mathematical sense,
   and if it is infinite, then its cardinality doesn't behave as expected (namely, not equal to the
-  field extension degree of `separableClosure F E / F`). For example,
-  $\operatorname{Emb}_{\mathbb{Q}}(\mathbb{Q}(\mu_{p^\infty}))\cong\mathbb{Z}_p^\times$ which is
-  uncountable, while $[\mathbb{Q}(\mu_{p^\infty}):\mathbb{Q}]$ is countable.
+  field extension degree of `separableClosure F E / F`). For example, if $ F = \mathbb{Q} $ and
+  $ E = \mathbb{Q}( \mu_{p^\infty} ) $, then $ \operatorname{Emb}_F (E) $ is in bijection with
+  $\operatorname{Gal}(E/F)$, which is isomorphic to
+  $ \mathbb{Z}_p^\times $, which is uncountable, while $ [E:F] $ is countable.
 
   **TODO:** prove or disprove that if `E / F` is algebraic and `Emb F E` is infinite, then
   `Field.Emb F E` has cardinality `2 ^ Module.rank F (separableClosure F E)`.