Theorem Mathlib.Tactic.MonTauto.associator_inv_comp_tensorHom_tensorHom_comp

Modification history

2025-08-28 09:43
Mathlib/CategoryTheory/Monoidal/Mon_.lean
feat: `mon_tauto`, a simp set to prove tautologies about a monoid object (#26057) …
Added Mathlib.Tactic.MonTauto.associator_inv_comp_tensorHom_tensorHom_compView on Github →