Update README.md

mbkybky · Oct 26, 2024 · 889031b · 889031b
1 parent 7b07b3f
commit 889031b
Showing 1 changed file with 4 additions and 2 deletions.
diff --git a/README.md b/README.md
@@ -1,3 +1,5 @@
-# Ramification theory in Galois extensions of Dedekind domains
+# Formalizing ramification theory in Galois extensions in LEAN 4
 
-Formalizing the ramification theory in Galois extensions of Dedekind domains, which is also called Hilbert's Ramification Theory.
+Formalizing the ramification theory in Galois extensions of Dedekind domains, which is also called Hilbert's ramification theory.
+
+The case of ramification theory in Galois extensions of number fields is ported from the [Neukirch, Algebraic Number Theory](https://github.com/jjdishere/neukirch/blob/master/AlgebraicNumberTheory/AlgebraicIntegersPart2/HilbertRamificationTheory.lean) project.