Commit 2022-12-14 15:48 49c4ff2d

View on Github →

feat port: Data.Nat.Cast.WithTop (#1019) ee0c179cd3c8a45aa5bffbf1b41d8dbede452865

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Nat/Cast/WithTop.lean

added theorem Nat.cast_withBot

added theorem Nat.cast_withTop