Commit 2022-12-14 15:48 d70b81e8

View on Github →

feat port: Data.Nat.Upto (#1020) ee0c179cd3c8a45aa5bffbf1b41d8dbede452865

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Nat/Upto.lean

added def Nat.Upto.succ

added def Nat.Upto.zero

added def Nat.Upto