add_torsor): generalize to semi_normed_space (#7016)

Commit

4 years ago

refactor(analysis/normed_space/add_torsor): generalize to semi_normed_space (#7016) This part of a series of PR to include the theory of `semi_normed_space` in mathlib.

Author

riccardobrasca

Parents

c5ea4cdd

mathlib 9c2a3e7e - refactor(analysis/normed_space/add_torsor): generalize to semi_normed_space (#7016)

mathlib
9c2a3e7e - refactor(analysis/normed_space/add_torsor): generalize to semi_normed_space (#7016)