Def WithZeroMulInt.toNNReal

Modification history

2024-11-11 15:53

Mathlib/Data/Int/WithZero.lean

feat(Data/Int/WithZero): add API (#18668) …

Modified WithZeroMulInt.toNNReal View on Github →

2024-10-04 14:05

Mathlib/Data/Int/WithZero.lean

feat(Data/Int/WithZero): add WithZeroMultIntToNNReal (#15741) …

Added WithZeroMulInt.toNNReal View on Github →