[Merged by Bors] - feat: Mixins for monotonicity of scalar multiplication

[YaelDillies]

This PR introduces eight typeclasses for monotonicity of left/right scalar multiplication by nonnegative elements:

• PosSMulMono: If a ≥ 0, then b₁ ≤ b₂ implies a • b₁ ≤ a • b₂.
• PosSMulStrictMono: If a > 0, then b₁ < b₂ implies a • b₁ < a • b₂.
• PosSMulReflectLT: If a ≥ 0, then a • b₁ < a • b₂ implies b₁ < b₂.
• PosSMulReflectLE: If a > 0, then a • b₁ ≤ a • b₂ implies b₁ ≤ b₂.
• SMulPosMono: If b ≥ 0, then a₁ ≤ a₂ implies a₁ • b ≤ a₂ • b.
• SMulPosStrictMono: If b > 0, then a₁ < a₂ implies a₁ • b < a₂ • b.
• SMulPosReflectLT: If b ≥ 0, then a₁ • b < a₂ • b implies a₁ < a₂.
• SMulPosReflectLE: If b > 0, then a₁ • b ≤ a₂ • b implies a₁ ≤ a₂.

The design is heavily inspired to the corresponding one for multiplication (see Algebra.Order.Ring.Lemmas). Note however the following differences:

• The new typeclasses are custom typeclasses instead of abbreviations for the correct CovariantClass/ContravariantClass invokations. This has the following benefits:
  • They get displayed as classes in the docs. In particular, one can see their list of instances, instead of their instances being invariably dumped to the CovariantClass/ContravariantClass list.
  • They don't pollute other typeclass searches. Having many abbreviations of the same typeclass for different purposes always felt like a performance issue to me (more instances with the same key, for no added benefit), and indeed a previous version of this PR hit timeouts due to the higher number of CovariantClass/ContravariantClass instances.
  • SMulPosReflectLT/SMulPosReflectLE did not fit in the framework since they relate ≤ on two different types. So I would have had to generalise CovariantClass/ContravariantClass to three types and two relations.
  • Very minor, but the constructors let you work with a : α, h : 0 ≤ a instead of a : {a : α // 0 ≤ a}. This actually makes some instances surprisingly cleaner to prove.
  • The CovariantClass/ContravariantClass framework was only used to automate very simple logic anyway. It was easily copied over.
• We replace undocumented lemmas stating the equivalence of the four typeclasses mentioning nonnegativity with their positivity version by motivated constructors.
• We abandon series of lemmas of dubious utility. Those were already marked as such in Algebra.Order.Ring.Lemmas (by myself).
• Some lemmas about commutativity of multiplication don't make sense for scalar multiplication.

This PR links the new typeclasses to OrderedSMul and makes all old lemmas in Algebra.Order.SMul one-liners in terms of the new lemmas (except when they have the same name, in which case the lemma is simply moved) but doesn't delete the old ones to reduce churn. What remains to be done afterwards is thus:

• finish the transition by deleting the duplicate lemmas from Algebra.Order.SMul
• rearrange the non-duplicate lemmas into new files
• generalise (most of) the lemmas from Algebra.Order.Module to Algebra.Order.Module.Defs
• rethink OrderedSMul

---

[eric-wieser]

• ...MonoRev is replaced by ...ReflectLE in the hope of being more understandable.

Can you spin out a PR to make this change to the Mul typeclasses first?

[YaelDillies]

#8890

[eric-wieser]

This PR also:

• deletes instModuleOrderDual, which was accidentally duplicated in [Merged by Bors] - chore: Move OrderDual action instances to their own file #8840.
• fixes the dead links to Wikipedia in Algebra.Order.SMul and Algebra.Order.Module.

This looks like an easy spin-off too.

[YaelDillies]

#8902

[jcommelin]

!bench

[jcommelin]

Hmm, that !bench isn't going to measure anything, because this new API isn't really used yet.

bors merge

[leanprover-bot]

Here are the benchmark results for commit 018bda8.
There were significant changes against commit 31037d9:

  Benchmark                                         Metric                 Change
  ===============================================================================
- build                                             .olean serialization     6.3%
- build                                             import                   5.7%
- build                                             initialization           5.4%
- open Mathlib                                      instructions             5.5%
- open Mathlib                                      task-clock              31.1%
- ~Mathlib.Analysis.NormedSpace.Multilinear.Basic   instructions             2.3%

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style
• Check all files imported