Theorem CategoryTheory.MonoidalCategory.MonoidalRightAction.actionUnitIso_inv_naturality

Modification history

2025-06-22 20:25
Mathlib/CategoryTheory/Monoidal/Action/Basic.lean
feat(CategoryTheory/Monoidal/Action): monoidal right actions (#25840) …
Added CategoryTheory.MonoidalCategory.MonoidalRightAction.actionUnitIso_inv_naturalityView on Github →