Commit 2023-05-26 16:13 e0736bb5

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.