Commit 2023-10-30 15:05 baf4bc6f

View on Github →

feat: Basic lemmas about positivity of a • b (#7647) All lemmas and lemma names are taken from their mul counterpart.

Estimated changes

Modified Mathlib/Algebra/Order/Module.lean

added theorem nonneg_and_nonneg_or_nonpos_and_nonpos_of_smul_nonneg

added theorem smul_le_smul

added theorem smul_le_smul_of_nonneg_right

added theorem smul_nonneg_iff

added theorem smul_nonneg_iff_neg_imp_nonpos

added theorem smul_nonneg_iff_pos_imp_nonneg

added theorem smul_nonpos_iff

added theorem smul_nonpos_iff_neg_imp_nonneg

added theorem smul_nonpos_iff_pos_imp_nonpos

Modified Mathlib/Algebra/Order/SMul.lean