Commit 2025-06-02 16:49 41239f9f
View on Github →feat(Mathlib/Analysis/Normed/Group/InfiniteSum): add versions of lemmas for enorm (#25371)
Several lemmas added, each concerns enorm
and is the direct equivalent of lemmas which already exist for norm
.