Ordered module #
In this file we provide lemmas about
ordered_smul that hold once a module structure is present.
ordered module, ordered scalar, ordered smul, ordered action, ordered vector space
Alias of the reverse direction of smul_pos_iff_of_neg`.
Alias of the reverse direction of smul_neg_iff_of_pos`.
Alias of the reverse direction of smul_neg_iff_of_neg`.
Left scalar multiplication as an order isomorphism.