Commit 2022-02-04 18:53 5b3cd4a9
View on Github →refactor(analysis/normed_space/add_torsor): Kill seminormed_add_torsor (#11795)
Delete normed_add_torsor in favor of the equivalent seminormed_add_torsor and rename seminormed_add_torsor to normed_add_torsor.