In this repo, we formalize in Lean 4 the result that the p-adic complex number field (\mathbb{C}_p) is algebraically closed.
This work depends on the repo https://github.com/mariainesdff/LocalClassFieldTheory.
jjdishere/CPAlgClosed
Folders and files
| Name | Name | Last commit date | ||
|---|---|---|---|---|