doc: add an algebraic number theory section to Mathlib overview (#7429)

leanprover-community · Oct 4, 2023 · 5eb7748 · 5eb7748
1 parent 39a866a
commit 5eb7748
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 1 deletion.
diff --git a/Mathlib/NumberTheory/NumberField/ClassNumber.lean b/Mathlib/NumberTheory/NumberField/ClassNumber.lean
@@ -28,7 +28,7 @@ variable (K : Type*) [Field K] [NumberField K]
 
 namespace RingOfIntegers
 
-noncomputable instance : Fintype (ClassGroup (ringOfIntegers K)) :=
+noncomputable instance instFintypeClassGroup : Fintype (ClassGroup (ringOfIntegers K)) :=
   ClassGroup.fintypeOfAdmissibleOfFinite ℚ K AbsoluteValue.absIsAdmissible
 
 end RingOfIntegers

diff --git a/docs/overview.yaml b/docs/overview.yaml
@@ -139,6 +139,10 @@ General algebra:
   Transcendental numbers:
     Liouville's theorem on existence of transcendental numbers: 'transcendental_liouvilleNumber'
 
+  Algebraic Number Theory:
+    Finiteness of the class number: 'NumberField.RingOfIntegers.instFintypeClassGroup'
+    Dirichlet unit theorem: 'NumberField.Units.exist_unique_eq_mul_prod'
+
   Representation theory:
     representation : 'Representation'
     category of finite dimensional representations : 'FdRep'