Commit 2023-05-25 18:32 de83b437
View on Github →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.