Commit 2025-07-14 10:26 8d72c490

View on Github →

chore(CategoryTheory): rename tensor_id to id_tensorHom_id (#27122) This is simply misnamed. From Toric

Estimated changes

Modified Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean

added theorem ModuleCat.MonoidalCategory.id_tensorHom_id

deleted theorem ModuleCat.MonoidalCategory.tensor_id

Modified Mathlib/Algebra/Category/ModuleCat/Presheaf/Monoidal.lean

Modified Mathlib/CategoryTheory/Dialectica/Monoidal.lean

added theorem CategoryTheory.Dial.id_tensorHom_id

deleted theorem CategoryTheory.Dial.tensor_id

Modified Mathlib/CategoryTheory/GradedObject/Monoidal.lean

added theorem CategoryTheory.GradedObject.Monoidal.id_tensorHom_id

deleted theorem CategoryTheory.GradedObject.Monoidal.tensor_id

Modified Mathlib/CategoryTheory/Localization/Monoidal.lean

added theorem CategoryTheory.Localization.Monoidal.id_tensorHom_id

deleted theorem CategoryTheory.Localization.Monoidal.tensor_id

Modified Mathlib/CategoryTheory/Monoidal/Cartesian/Basic.lean

added theorem CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.id_tensorHom_id

deleted theorem CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensor_id

Modified Mathlib/CategoryTheory/Monoidal/Category.lean

Modified Mathlib/CategoryTheory/Monoidal/Free/Basic.lean

Modified Mathlib/CategoryTheory/Monoidal/Preadditive.lean

Modified Mathlib/CategoryTheory/Monoidal/Transport.lean

Modified Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat/Monoidal.lean