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 project.