feat: port NumberTheory.Padics.Hensel (#4344)

This file makes heavy use of `parameter` and `include` that do not exist in Lean4 thus many arguments have to provided explicitly. In some cases where this would have been too heavy, I used `local notation` instead, see [this](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/!4.234344.20NumberTheory.2EPadics.2EHensel/near/361119207) Zulip thread.
leanprover-community · May 26, 2023 · 51b5453 · 51b5453
1 parent 7442e24
commit 51b5453
Show file tree

Hide file tree

Showing 2 changed files with 506 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1865,6 +1865,7 @@ import Mathlib.NumberTheory.LucasLehmer
 import Mathlib.NumberTheory.LucasPrimality
 import Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
 import Mathlib.NumberTheory.Multiplicity
+import Mathlib.NumberTheory.Padics.Hensel
 import Mathlib.NumberTheory.Padics.PadicIntegers
 import Mathlib.NumberTheory.Padics.PadicNorm
 import Mathlib.NumberTheory.Padics.PadicNumbers