Def WithZeroMulInt.toNNReal

Modification history

2025-07-04 09:20

Mathlib/Data/Int/WithZero.lean

feat(WithZero): `exp : ℤ → ℤᵐ⁰`, `log : ℤᵐ⁰ → ℤ` (#24977) …

Modified WithZeroMulInt.toNNReal View on Github →

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 →