mathlib

acc1d4bd - feat(analysis/normed_space/SemiNormedGroup/kernels) : add lemmas (#9654)