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.

Estimated changes