Commit 2022-09-21 15:26 b1539919

View on Github →

doc(metric_space/basic): modify doc for metric spaces adding pseudo metric spaces (#16577) The doc preceeding the pseudo_metric_space instance spoke only about metric spaces. I have added the pseudo_metric version.

Estimated changes