feat(analysis/seminorm): smul_sup (#12103)
feat(analysis/seminorm): smul_sup (#12103)

The `have : real.smul_max` local proof doesn't feel very general, so I've left it as a `have` rather than promoting it to a lemma.





leanprover-community/mathlib,leanprover-community/mathlib