Def castPosNum

Modification history

2024-06-04 13:47

Mathlib/Data/Num/Basic.lean

chore: add dates to more deprecations (#13186) …

Modified castPosNum View on Github →

2023-03-31 13:00

Mathlib/Data/Num/Basic.lean

refactor: Refactor coercions in `Data.Num.Basic` (#2780) …

Modified castPosNum View on Github →

2022-11-18 00:25

Mathlib/Data/Num/Basic.lean

feat: port data.num.basic (#607) …

Added castPosNum View on Github →