feat: port NumberTheory.Multiplicity (#4044)

Co-authored-by: Moritz Firsching <firsching@google.com> Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>
leanprover-community · May 18, 2023 · c39117e · c39117e
1 parent 870cc2b
commit c39117e
Show file tree

Hide file tree

Showing 2 changed files with 422 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1667,6 +1667,7 @@ import Mathlib.NumberTheory.Fermat4
 import Mathlib.NumberTheory.FrobeniusNumber
 import Mathlib.NumberTheory.LucasLehmer
 import Mathlib.NumberTheory.LucasPrimality
+import Mathlib.NumberTheory.Multiplicity
 import Mathlib.NumberTheory.Padics.PadicNorm
 import Mathlib.NumberTheory.Padics.PadicVal
 import Mathlib.NumberTheory.PellMatiyasevic