2025-05-14 15:37
Mathlib/CategoryTheory/ChosenFiniteProducts.lean
refactor: move the construction of `ChosenFiniteProducts` from finite products with `ChosenFiniteProducts` (#24679) …
Added CategoryTheory.ChosenFiniteProducts.ofChosenFiniteProducts.tensor_comp