mathlib3
refactor(topology/metric/gromov_hausdorff): make Hausdorff_edist irreducible
#1052
Merged
Overview
Commits
3
Changes
View On GitHub

refactor(topology/metric/gromov_hausdorff): make Hausdorff_edist irreducible #1052

mergify merged 3 commits into leanprover-community:master from sgouezel:speedup_gromov_hausdorff
sgouezel
sgouezel refactor(topology/metric/gromov_hausdorff): remove linarith calls
6bbb3281
sgouezel sgouezel requested a review 6 years ago
sgouezel sgouezel added WIP
sgouezel refactor(topology/metric/hausdorff_dist): make hausdorff_dist irreduc…
1250f3a4
sgouezel sgouezel changed the title refactor(topology/metric/gromov_hausdorff): remove linarith calls refactor(topology/metric/gromov_hausdorff): make Hausdorff_edist irreducible 6 years ago
sgouezel sgouezel removed WIP
robertylewis
robertylewis approved these changes on 2019-05-19
robertylewis robertylewis added ready-to-merge
Merge branch 'master' into 'speedup_gromov_hausdorff'
d4d062b8
mergify mergify merged cb4c9ee7 into master 6 years ago
sgouezel sgouezel deleted the speedup_gromov_hausdorff branch 6 years ago

Login to write a write a comment.

Login via GitHub

Reviewers
Assignees
No one assigned
Labels
ready-to-merge
Milestone
No milestone
Terms Of Use Privacy Policy Refund Policy Impressum