mathlib3
[Merged by Bors] - chore(category_theory/concrete_category): reorder universes
#19222
Closed
Overview
Commits
1
Changes
View On GitHub

[Merged by Bors] - chore(category_theory/concrete_category): reorder universes #19222

kim-em wants to merge 1 commit into master from reorder_universes_concrete
kim-em
kim-em chore(category_theory/concrete_category): reorder universes
73b1aeb4
kim-em kim-em added awaiting-review
kim-em kim-em added awaiting-CI
kim-em kim-em requested a review 2 years ago
github-actions github-actions added modifies-synchronized-file
github-actions github-actions removed awaiting-CI
jcommelin
github-actions github-actions added ready-to-merge
github-actions github-actions removed awaiting-review
bors
bors bors changed the title chore(category_theory/concrete_category): reorder universes [Merged by Bors] - chore(category_theory/concrete_category): reorder universes 2 years ago
bors bors closed this 2 years ago
bors bors deleted the reorder_universes_concrete branch 2 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