Theorem toZ_strictMono

Modification history

2026-05-10 00:45
Mathlib/Order/SuccPred/LinearLocallyFinite.lean
feat(Order/SuccPred/LinearLocallyFinite): `StrictMono toZ` (#39014) …
Added toZ_strictMonoView on Github →