Theorem CategoryTheory.ChosenFiniteProducts.ofChosenFiniteProducts.leftUnitor_naturality

Modification history

2025-05-15 18:47
Mathlib/CategoryTheory/Monoidal/Cartesian/Basic.lean
chore: rename `ChosenFiniteProducts` to `CartesianMonoidalCategory` (#24390) …
Deleted CategoryTheory.ChosenFiniteProducts.ofChosenFiniteProducts.leftUnitor_naturalityView on Github →
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.leftUnitor_naturalityView on Github →