Theorem PosMulMono.toMulPosMono

Modification history

2025-04-11 08:18

Mathlib/Algebra/Order/GroupWithZero/Unbundled/Defs.lean

feat(Order/GroupWithZero): drop more TC assumptions (#23922) …

Added PosMulMono.toMulPosMono View on Github →