Commit 2024-09-10 07:29 ba034836

View on Github →

feat(CategoryTheory/MonoidalComp): change IsIso to Iso (#16554) I'm planning a rewrite of the coherence tactics (a series of PR starting from #16562), and this PR is preparation for that.

Estimated changes

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

Modified Mathlib/CategoryTheory/Monoidal/Rigid/Braided.lean

Modified Mathlib/Tactic/CategoryTheory/Coherence.lean

Modified Mathlib/Tactic/CategoryTheory/Monoidal.lean

Modified Mathlib/Tactic/CategoryTheory/MonoidalComp.lean

deleted def CategoryTheory.monoidalIso