mathlib3
fix(topology/metric_space): fix uniform structure on Pi types
#1551
Merged
Merged
fix(topology/metric_space): fix uniform structure on Pi types #1551
mergify
merged
5 commits into
leanprover-community:master
from
sgouezel:pi_topology
fix(topology/metric_space): fix uniform structure on pi tpype
1b5adc78
cleanup
b7baf20e
digama0
commented
on 2019-10-14
better construction of metric from emetric
e7683e18
PatrickMassot
commented
on 2019-10-16
use simp only instead of simp
ac3557a2
PatrickMassot
approved these changes
on 2019-10-17
![mergify[bot]](https://avatars.githubusercontent.com/in/10562?v=4&s=60)
Merge branch 'master' into pi_topology
4c000798
Reviewers
Assignees
Labels
ready-to-merge
Milestone
No milestone
Login to write a write a comment.
Login via GitHub