Theorem WithZeroMulInt.toNNReal_pos_apply

Modification history

2024-11-11 15:53
Mathlib/Data/Int/WithZero.lean
feat(Data/Int/WithZero): add API (#18668) …
Modified WithZeroMulInt.toNNReal_pos_applyView on Github →
2024-10-04 14:05
Mathlib/Data/Int/WithZero.lean
feat(Data/Int/WithZero): add WithZeroMultIntToNNReal (#15741) …
Added WithZeroMulInt.toNNReal_pos_applyView on Github →