Skip to content

Commit a1c58a9

Browse files
feat: port Data.Nat.Squarefree (#4278)
Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
1 parent e53aed1 commit a1c58a9

File tree

2 files changed

+581
-0
lines changed

2 files changed

+581
-0
lines changed

Mathlib.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1243,6 +1243,7 @@ import Mathlib.Data.Nat.PrimeNormNum
12431243
import Mathlib.Data.Nat.Set
12441244
import Mathlib.Data.Nat.Size
12451245
import Mathlib.Data.Nat.Sqrt
1246+
import Mathlib.Data.Nat.Squarefree
12461247
import Mathlib.Data.Nat.SuccPred
12471248
import Mathlib.Data.Nat.Totient
12481249
import Mathlib.Data.Nat.Units

0 commit comments

Comments
 (0)