Commit 2022-02-08 22:14 56db7ed0
View on Github →feat(analysis/normed_space/basic): add lemmas nnnorm_mul_le and nnnorm_pow_succ_le (#11915)
Adds two convenience lemmas for nnnorm, submultiplicativity of nnnorm for semi-normed rings and the corresponding extension to powers. We only allow successors so as not to incur the norm_one_class type class constraint.