Theorem PosMulReflectLE.toMulPosReflectLE

Modification history

2025-04-11 08:18

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

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

Added PosMulReflectLE.toMulPosReflectLE View on Github →