Theorem mul_lt_mul_of_lt_of_le_of_pos_of_nonneg

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_lt_of_le_of_pos_of_nonneg View on Github →