Def CategoryTheory.ChosenFiniteProducts.ofFiniteProducts

Modification history

2025-05-07 21:03

Mathlib/CategoryTheory/ChosenFiniteProducts.lean

refactor(CategoryTheory): Make `ChosenFiniteProducts` extend `MonoidalCategory` (#24399) …

Deleted CategoryTheory.ChosenFiniteProducts.ofFiniteProducts View on Github →

2024-03-14 22:18

Mathlib/CategoryTheory/ChosenFiniteProducts.lean

feat: chosen finite products in a category (#11248) …

Added CategoryTheory.ChosenFiniteProducts.ofFiniteProducts View on Github →