mathlib

ba5ff5ad - refactor(analysis/normed_space/basic): generalize some results to actions by normed_rings (#19053)

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.