mathlib
5b3cd4a9 - refactor(analysis/normed_space/add_torsor): Kill `seminormed_add_torsor` (#11795)

Commit
3 years ago
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`.
Author
Parents
Loading