Commit 2025-08-16 12:53 35529d04

feat: e-seminormed monoid (#27385) Most lemmas about these do not require the enorm to be positive definite (i.e., work fine if a nontrivial element has zero enorm), or can be rephrased easily. A handful of lemmas do require this condition. Add a new class ESeminormed(Add)(Comm)Monoid, which only asks that zero have enorm, and generalise most lemmas to this class. The motivating example behind this is eLpNorm, which is an enormed commutative (additive) monoid