feat: port Data.Nat.Nth (#2297)

Co-authored-by: Komyyy <pol_tta@outlook.jp>
leanprover-community · Jun 25, 2023 · c534e06 · c534e06
1 parent 1cc9f36
commit c534e06
Show file tree

Hide file tree

Showing 2 changed files with 419 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1507,6 +1507,7 @@ import Mathlib.Data.Nat.Log
 import Mathlib.Data.Nat.MaxPowDiv
 import Mathlib.Data.Nat.ModEq
 import Mathlib.Data.Nat.Multiplicity
+import Mathlib.Data.Nat.Nth
 import Mathlib.Data.Nat.Order.Basic
 import Mathlib.Data.Nat.Order.Lemmas
 import Mathlib.Data.Nat.PSub