Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-08 23:06 75cc1ae9

View on Github →

feat(analysis/normed/group/basic): add norm_multiset_sum_le (#16419)

Estimated changes

Modified src/analysis/normed/group/basic.lean

added theorem nnnorm_multiset_sum_le

added theorem norm_multiset_sum_le