Theorem CategoryTheory.Functor.Monoidal.μ_comp

refactor(ChosenFiniteProducts): don't make finite-product-preserving functors monoidal (#24049) …

feat(CategoryTheory): forgetting the group structure on the codomain of left-exact functors (#21973) …