Theorem mul_lt_mul_of_le_of_lt_of_nonneg_of_pos

Modification history

2024-07-25 07:50

Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean

chore(Algebra/Order/GroupWithZero/Unbundled): resolving name inconsistencies (#9904) …

Added mul_lt_mul_of_le_of_lt_of_nonneg_of_pos View on Github →