basic): scaling a set scales its diameter, translating it leaves it unchanged (#18990)

Commit

2 years ago

feat(analysis/normed_space/basic): scaling a set scales its diameter, translating it leaves it unchanged (#18990)

Author

eric-wieser

Parents