docs: add Dirichlet class number formula to the overview (leanprover-community#25015)

Also add a `-` missing in the docstring of `tendsto_sub_one_mul_dedekindZeta_nhdsGT`

Author: xroblot

Mathlib/NumberTheory/NumberField/DedekindZeta.lean

@@ -65,7 +65,7 @@ theorem dedekindZeta_residue_pos : 0 < dedekindZeta_residue K := by
 theorem dedekindZeta_residue_ne_zero : dedekindZeta_residue K ≠ 0 :=
   (dedekindZeta_residue_pos K).ne'
 
-/-
+/--
 **Dirichlet class number formula**
 -/
 theorem tendsto_sub_one_mul_dedekindZeta_nhdsGT :

docs/overview.yaml

@@ -145,6 +145,7 @@ General algebra:
   Algebraic Number Theory:
     Finiteness of the class number: 'NumberField.RingOfIntegers.instFintypeClassGroup'
     Dirichlet unit theorem: 'NumberField.Units.exist_unique_eq_mul_prod'
+    Dirichlet class number formula: 'NumberField.tendsto_sub_one_mul_dedekindZeta_nhdsGT'
 
   Representation theory:
     representation : 'Representation'