isometry): rename `(e)metric.isometry.diam_image` to `isometry.(e)diam_image`
#2073

Merged

chore(topology/metric_space/isometry): rename `(e)metric.isometry.diam_image` to `isometry.(e)diam_image` #2073

mergify merged 2 commits into master from isometry-diam

chore(topology/metric_space/isometry): rename `(e)metric.isometry.dia…

b6ceb298

PatrickMassot approved these changes on 2020-03-02

PatrickMassot added ready-to-merge

Merge branch 'master' into isometry-diam

205d0cfe

mergify merged 3055b3c0 into master 5 years ago

mergify deleted the isometry-diam branch 5 years ago

Reviewers

PatrickMassot

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone