Commit 2020-10-20 08:10 617e8295

feat(linear_algebra/affine_space/ordered): define slope (#4669)

• Review API of ordered_semimodule:
  • replace lt_of_smul_lt_smul_of_nonneg with lt_of_smul_lt_smul_of_pos; it's equivalent but is easier to prove;
  • add more lemmas;
  • add a constructor for the special case of an ordered semimodule over a linearly ordered field; in this case it suffices to verify only a < b → 0 < c → c • a ≤ c • b;
  • use the new constructor in analysis/convex/cone;
• Define units.smul_perm_hom, reroute mul_action.to_perm through it;
• Add a few more lemmas unfolding affine_map.line_map in special cases;
• Define slope f a b = (b - a)⁻¹ • (f b -ᵥ f a) and prove a handful of monotonicity properties.