mathlib

1937dff0 - feat(analysis/normed_space/lp_space): normed_algebra structure (#15086)

feat(analysis/normed_space/lp_space): normed_algebra structure (#15086) This also golfs the `normed_ring` instance to go via `subring.to_ring`, as this saves us from having to build the power, nat_cast, and int_cast structures manually. We also rename `lp.lp_submodule` to `lp_submodule` to avoid unhelpful repetition.