feat: port NumberTheory.Liouville.LiouvilleWith (#4596)

leanprover-community · Jun 2, 2023 · 171df1e · 171df1e
1 parent 1c81f56
commit 171df1e
Show file tree

Hide file tree

Showing 2 changed files with 394 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1984,6 +1984,7 @@ import Mathlib.NumberTheory.LSeries
 import Mathlib.NumberTheory.LegendreSymbol.MulCharacter
 import Mathlib.NumberTheory.LegendreSymbol.ZModChar
 import Mathlib.NumberTheory.Liouville.Basic
+import Mathlib.NumberTheory.Liouville.LiouvilleWith
 import Mathlib.NumberTheory.Liouville.Residual
 import Mathlib.NumberTheory.LucasLehmer
 import Mathlib.NumberTheory.LucasPrimality