Skip to content

Commit 615e31f

Browse files
urkudKomyyy
andcommitted
feat: port Data.Nat.Nth (#2297)
Co-authored-by: Komyyy <pol_tta@outlook.jp>
1 parent 9da26a0 commit 615e31f

File tree

2 files changed

+419
-0
lines changed

2 files changed

+419
-0
lines changed

Mathlib.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1507,6 +1507,7 @@ import Mathlib.Data.Nat.Log
15071507
import Mathlib.Data.Nat.MaxPowDiv
15081508
import Mathlib.Data.Nat.ModEq
15091509
import Mathlib.Data.Nat.Multiplicity
1510+
import Mathlib.Data.Nat.Nth
15101511
import Mathlib.Data.Nat.Order.Basic
15111512
import Mathlib.Data.Nat.Order.Lemmas
15121513
import Mathlib.Data.Nat.PSub

0 commit comments

Comments
 (0)