Commit 2023-06-08 00:43 86ade6e9

View on Github →

chore: cleanup Discrete porting notes (#4780)

Estimated changes

Modified Mathlib/CategoryTheory/Adjunction/Comma.lean

Modified Mathlib/CategoryTheory/Category/Grpd.lean

Modified Mathlib/CategoryTheory/DiscreteCategory.lean

modified def CategoryTheory.Discrete.natIso

modified def CategoryTheory.Discrete.natTrans

Modified Mathlib/CategoryTheory/GradedObject.lean

Modified Mathlib/CategoryTheory/Limits/Constructions/Over/Products.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Products.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Types.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean

Modified Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean

Modified Mathlib/CategoryTheory/Monoidal/OfChosenFiniteProducts/Basic.lean

Modified Mathlib/CategoryTheory/Preadditive/Projective.lean

Modified Mathlib/CategoryTheory/StructuredArrow.lean