mathlib3
chore(topology/*): @uniformity α _ becomes 𝓤 α
#814

Merged

chore(topology/*): @uniformity α _ becomes 𝓤 α #814

johoelzl merged 1 commit into master from uniformity

chore(topology/*): @uniformity α _ becomes 𝓤 α

1c177207

PatrickMassot requested a review from

johoelzl 6 years ago

johoelzl merged 2738f9b4 into master 6 years ago

johoelzl deleted the uniformity branch 6 years ago

Reviewers

johoelzl

Assignees

No one assigned

Labels

None yet

Milestone

No milestone