mathlib

6298a431 - 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.