Theorem PosMulReflectLT.toMulPosReflectLT

Modification history

2025-04-11 08:18

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

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

Added PosMulReflectLT.toMulPosReflectLT View on Github →