Theorem CategoryTheory.Localization.Monoidal.tensor_id

Modification history

2025-07-14 10:26
Mathlib/CategoryTheory/Localization/Monoidal.lean
chore(CategoryTheory): rename `tensor_id` to `id_tensorHom_id` (#27122) …
Deleted CategoryTheory.Localization.Monoidal.tensor_idView on Github →
2025-06-16 16:23
Mathlib/CategoryTheory/Localization/Monoidal.lean
perf(CategoryTheory/Monoidal): change notations for tensor product of (iso)morphisms (#25922) …
Modified CategoryTheory.Localization.Monoidal.tensor_idView on Github →
2025-01-31 17:41
Mathlib/CategoryTheory/Localization/Monoidal.lean
feat(CategoryTheory): the monoidal category structure on a localization (#20951) …
Added CategoryTheory.Localization.Monoidal.tensor_idView on Github →