doc(FieldTheory/IsAlgClosed/Basic): add a TODO (#9519)

... which is: prove that if `K / k` is algebraic, and any monic irreducible polynomial over `k` has a root in `K`, then `K` is algebraically closed (in fact an algebraic closure of `k`). Reference: <https://kconrad.math.uconn.edu/blurbs/galoistheory/algclosure.pdf>, Theorem 2. From the reference it looks like that the proof of this result needs purely inseparable argument, so probably it can't be done in this file.
leanprover-community · Jan 8, 2024 · 70edc53 · 70edc53
1 parent 3b8d080
commit 70edc53
Showing 1 changed file with 7 additions and 0 deletions.
diff --git a/Mathlib/FieldTheory/IsAlgClosed/Basic.lean b/Mathlib/FieldTheory/IsAlgClosed/Basic.lean
@@ -34,6 +34,13 @@ polynomial in `k` splits.
 
 algebraic closure, algebraically closed
 
+## TODO
+
+- Prove that if `K / k` is algebraic, and any monic irreducible polynomial over `k` has a root
+  in `K`, then `K` is algebraically closed (in fact an algebraic closure of `k`).
+
+  Reference: <https://kconrad.math.uconn.edu/blurbs/galoistheory/algclosure.pdf>, Theorem 2
+
 -/