Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-07 08:01 6b0c73a0

View on Github →

chore(analysis/normed_space): add dist_sum_sum_le (#9049)

Estimated changes

added theorem dist_sum_sum_le
added theorem dist_sum_sum_le_of_le