mathlib3

de83b437 - feat(analysis/normed_space/lp_space): generalize from normed_field to `normed_ring` (#19085)

feat(analysis/normed_space/lp_space): generalize from normed_field to `normed_ring` (#19085) This provides a `module 𝕜 (lp E p)` instance for `normed_ring 𝕜` instead of `normed_field 𝕜`, as we didn't actually require that the bound on the norm of the scalar action was tight.