Theorem CategoryTheory.Localization.HasProductsOfShapeAux.adj_counit_app

Modification history

2024-02-09 04:56
Mathlib/CategoryTheory/Localization/FiniteProducts.lean
feat(CategoryTheory/Localization): the localized category has finite products (#9692) …
Added CategoryTheory.Localization.HasProductsOfShapeAux.adj_counit_appView on Github →