Commit 2022-07-08 13:36 1937dff0
View on Github →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.