Commit 2022-09-30 13:10 64ad902d
View on Github →refactor(algebra/order/{smul,module}): Turn lemmas around (#16696)
Match the mul lemmas by having the ⁻¹ on the LHS in inv_smul_le_iff, inv_smul_lt_iff, etc... Also generalize for free to ordered_add_comm_monoid.