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
.