feat: port NumberTheory.ZetaFunction (#5556)

leanprover-community · Jun 29, 2023 · 584c909 · 584c909
1 parent 5e6d910
commit 584c909
Show file tree

Hide file tree

Showing 2 changed files with 808 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -2412,6 +2412,7 @@ import Mathlib.NumberTheory.SumTwoSquares
 import Mathlib.NumberTheory.VonMangoldt
 import Mathlib.NumberTheory.WellApproximable
 import Mathlib.NumberTheory.Wilson
+import Mathlib.NumberTheory.ZetaFunction
 import Mathlib.NumberTheory.ZetaValues
 import Mathlib.NumberTheory.Zsqrtd.Basic
 import Mathlib.NumberTheory.Zsqrtd.GaussianInt