mathlib3
[Merged by Bors] - chore(topology/sheaves/*): universe generalizations
#19153
Closed
Overview
Commits
3
Changes
View On GitHub

[Merged by Bors] - chore(topology/sheaves/*): universe generalizations #19153

kim-em wants to merge 3 commits into master from sheaf_universes
kim-em
kim-em chore(topology/sheaves/*): universe generalizations
b5840cd6
kim-em kim-em requested a review 3 years ago
kim-em kim-em requested a review 3 years ago
kim-em kim-em added awaiting-review
kim-em kim-em added awaiting-CI
kim-em kim-em added modifies-synchronized-file
kim-em oops
689bdbba
kim-em oops
ca4f2896
github-actions github-actions removed awaiting-CI
hrmacbeth
github-actions github-actions added ready-to-merge
github-actions github-actions removed awaiting-review
bors
bors bors changed the title chore(topology/sheaves/*): universe generalizations [Merged by Bors] - chore(topology/sheaves/*): universe generalizations 3 years ago
bors bors closed this 3 years ago
bors bors deleted the sheaf_universes branch 3 years ago

Login to write a write a comment.

Login via GitHub

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