Commit 2022-02-21 00:51 6298a431
View on Github →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.
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.