Commit 2023-03-08 11:50 29806653
View on Github →feat: add NatCast, IntCast, and NatSucc positivity extensions (#2402)
- Adds positivity extensions for casting from nats and ints, corresponding to this mathlib3 code.
- Adds positivity extension for Nat.succ, corresponding to this mathlib3 code.