Theorem PosMulMono.toPosMulStrictMono

Modification history

2025-02-19 19:52

Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean

perf: turn `PosMulMono` and friends into classes (#22090) …

Modified PosMulMono.toPosMulStrictMono View on Github →

2022-11-23 19:15

Mathlib/Algebra/Order/Ring/Lemmas.lean

feat: port Algebra.Order.Ring.Lemmas (#482) …

Added PosMulMono.toPosMulStrictMono View on Github →