mathlib

e0736bb5 - refactor(measure_theory/function/lp_space): generalize actions from `normed_field` to `normed_ring` (#19083)

refactor(measure_theory/function/lp_space): generalize actions from `normed_field` to `normed_ring` (#19083) The motivation is that this makes it easier to work with integrals in non-commutative rings. This makes the proof of Hölder's inequality slightly more painful, as we can no longer use `simp_rw [norm_smul]` and have to make monotonicity arguments instead. `rel_congr` may be able to clean this up in mathlib3. The results in the `normed_space` section (including Hölder's inequality) have been largely moved to the `monotonicity` section, where they hold more generally for arbitrary binary functions. The results about scalar actions now follow as trivial special cases. This also makes the `fails_quickly` linter reject the `complete_space (Lp_meas F 𝕜 m p μ)` instance. Since Lean4 is around the corner and there are better debugging tools there, I think it's ok to just no-lint it.