Commit 2024-11-11 15:53 e80d8fc2

View on Github →

feat(Data/Int/WithZero): add API (#18668) In this PR we add three basic facts about WithZeroMultInt.toNNReal.

Estimated changes

Modified Mathlib/Data/Int/WithZero.lean

modified def WithZeroMulInt.toNNReal

added theorem WithZeroMulInt.toNNReal_eq_one_iff

added theorem WithZeroMulInt.toNNReal_le_one_iff

added theorem WithZeroMulInt.toNNReal_lt_one_iff

modified theorem WithZeroMulInt.toNNReal_ne_zero

modified theorem WithZeroMulInt.toNNReal_neg_apply

modified theorem WithZeroMulInt.toNNReal_pos

modified theorem WithZeroMulInt.toNNReal_pos_apply

modified theorem WithZeroMulInt.toNNReal_strictMono