Commit 2021-05-18 04:50 1a2781a7

View on Github →

feat(analysis/normed_space): the category of seminormed groups (#7617) From LTE, along with adding SemiNormedGroup₁, the subcategory of norm non-increasing maps.

Estimated changes