Commit 2024-08-29 18:57 606cfb3a

View on Github →

feat(CategoryTheory/Monoida): add lemmas for tensorIso (#15681) Also rename CategoryTheory.tensorIso to CategoryTheory.MonoidalCategory.tensorIso.

Estimated changes

Modified Mathlib/Algebra/Category/AlgebraCat/Monoidal.lean

Modified Mathlib/CategoryTheory/Monoidal/Category.lean

added def CategoryTheory.MonoidalCategory.tensorIso

added theorem CategoryTheory.MonoidalCategory.tensorIso_def'

added theorem CategoryTheory.MonoidalCategory.tensorIso_def

deleted def CategoryTheory.tensorIso

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