From 288b6c5536e3a1c520aff20a999fe55a627c9637 Mon Sep 17 00:00:00 2001
From: Jz Pan <acme_pjz@hotmail.com>
Date: Thu, 28 Dec 2023 21:07:40 +0000
Subject: [PATCH] doc(FieldTheory/SeparableDegree): fix the formula in
 docstring (#9318)

---
 Mathlib/FieldTheory/SeparableDegree.lean | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/Mathlib/FieldTheory/SeparableDegree.lean b/Mathlib/FieldTheory/SeparableDegree.lean
index 43ac871242137..a401c7593796e 100644
--- a/Mathlib/FieldTheory/SeparableDegree.lean
+++ b/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)`.