Commit 2023-05-23 16:54 ba5ff5ad

refactor(analysis/normed_space/basic): generalize some results to actions by normed_rings (#19053) This only moves the very basic lemmas for now. This should be very easy to forward-port:

• Let someone port the new file via the normal mechanism
• Have them delete the duplicate lemmas that appear in CI A few downstream proofs need some small help with unification, as while the old normed_space argument was found by unification, the new has_bounded_smul has to be found by typeclass search.