Commit 2025-04-09 21:31 25ffff65

View on Github →

feat(ChosenFiniteProducts): functoriality of prodComparisonIso (#23871) Also make NatTrans.monoidal_of_preservesFiniteProducts an instance since it's not data-carrying. From Toric

Estimated changes

Modified Mathlib/CategoryTheory/ChosenFiniteProducts.lean

deleted theorem CategoryTheory.ChosenFiniteProducts.map_toUnit_comp_terminalCompariso

added theorem CategoryTheory.ChosenFiniteProducts.map_toUnit_comp_terminalComparison

added theorem CategoryTheory.ChosenFiniteProducts.preservesTerminalIso_comp

added theorem CategoryTheory.ChosenFiniteProducts.preservesTerminalIso_id

added theorem CategoryTheory.ChosenFiniteProducts.prodComparisonIso_comp

added theorem CategoryTheory.ChosenFiniteProducts.prodComparisonIso_id

deleted theorem CategoryTheory.Functor.EssImageSubcategory.NatTrans.monoidal_of_preservesFiniteProducts

added theorem CategoryTheory.Functor.Monoidal.ε_of_chosenFiniteProducts

modified theorem CategoryTheory.Functor.Monoidal.μ_fst

added theorem CategoryTheory.Functor.Monoidal.μ_of_chosenFiniteProducts

modified theorem CategoryTheory.Functor.Monoidal.μ_snd

Modified Mathlib/CategoryTheory/Monoidal/CommGrp_.lean

Modified Mathlib/CategoryTheory/Monoidal/Grp_.lean