mathlib

617e8295 - feat(linear_algebra/affine_space/ordered): define `slope` (#4669)

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.