New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - chore: Generalise monotonicity of •
lemmas in modules
#9241
Conversation
Sort the lemmas in `Algebra.Order.Module` into `Algebra.Order.Module.Defs` and `Algebra.Order.Module.Pointwise`. Generalise them. A later PR will rename the lemmas to better match the naming convention.
exact smul_lt_smul_of_pos_left hb (neg_pos_of_neg ha) | ||
#align smul_lt_smul_of_neg smul_lt_smul_of_neg | ||
|
||
lemma strict_anti_smul_left (ha : a < 0) : StrictAnti (SMul.smul a : β → β) := |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
lemma strict_anti_smul_left (ha : a < 0) : StrictAnti (SMul.smul a : β → β) := | |
lemma strictAnti_smul_left (ha : a < 0) : StrictAnti (SMul.smul a : β → β) := |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is on my TODO list, but I'm not renaming anything in this PR!
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks 🎉
bors merge
Sort the lemmas in `Algebra.Order.Module` into `Algebra.Order.Module.Defs` and `Algebra.Order.Module.Pointwise`. Generalise them. A later PR will rename the lemmas to better match the naming convention.
Pull request successfully merged into master. Build succeeded: |
•
lemmas in modules•
lemmas in modules
Fix the names of the lemmas moved in #9241 to match the naming convention.
Fix the names of the lemmas moved in #9241 to match the naming convention.
Sort the lemmas in
Algebra.Order.Module
intoAlgebra.Order.Module.Defs
andAlgebra.Order.Module.Pointwise
. Generalise them.A later PR will rename the lemmas to better match the naming convention.