Commit 2022-04-29 17:28 8624f6db
View on Github →chore(analysis/normed/group/basic): add nnnorm_sum_le_of_le (#13795)
This is to match norm_sum_le_of_le.
Also tidies up the coercion syntax a little in pi.semi_normed_group.
The definition is syntactically identical, just with fewer unecessary type annotations.