mathlib3
chore(topology): Splits topology.basic and topology.continuity
#785
Merged
Overview
Commits
1
Changes
View On GitHub

chore(topology): Splits topology.basic and topology.continuity #785

johoelzl merged 1 commit into master from top_split_again
PatrickMassot
PatrickMassot chore(topology): Splits topology.basic and topology.continuity
675578e2
PatrickMassot PatrickMassot requested a review from johoelzl johoelzl 6 years ago
PatrickMassot PatrickMassot requested a review from rwbarton rwbarton 6 years ago
johoelzl
johoelzl
johoelzl approved these changes on 2019-03-03
sgouezel
PatrickMassot
johoelzl johoelzl merged 201413b9 into master 6 years ago
johoelzl johoelzl deleted the top_split_again branch 6 years ago
johoelzl
PatrickMassot

Login to write a write a comment.

Login via GitHub

Reviewers
Assignees
No one assigned
Labels
None yet
Milestone
No milestone
Terms Of Use Privacy Policy Refund Policy Impressum