Commit 2023-06-30 06:08 e9eb901c

View on Github →

chore: reorder universes in ConcreteCategory (#5605)

Estimated changes

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

Modified Mathlib/CategoryTheory/ConcreteCategory/Basic.lean

modified def CategoryTheory.ConcreteCategory.hasCoeToSort

modified def CategoryTheory.forget