Basic

📁 Source: Mathlib/CategoryTheory/Monoidal/Action/Basic.lean

Statistics

Metric	Count
Definitions `MonoidalLeftAction`, `actionAssocNatIso`, `actionLeft`, `actionRight`, `actionUnitNatIso`, `curriedAction`, `termαₗ`, `toMonoidalLeftActionStruct`, `«term_⊙ₗ_»`, `«term_⊙ₗₘ_»`, `«term_⊴ₗ_»`, `«term_⊵ₗ_»`, `«termλₗ[_]»`, `«termλₗ»`, `MonoidalLeftActionStruct`, `actionAssocIso`, `actionHom`, `actionHomLeft`, `actionHomRight`, `actionObj`, `actionUnitIso`, `MonoidalRightAction`, `actionAssocNatIso`, `actionLeft`, `actionRight`, `actionUnitNatIso`, `curriedAction`, `termαᵣ`, `termρᵣ`, `toMonoidalRightActionStruct`, `«term_⊙ᵣ_»`, `«term_⊙ᵣₘ_»`, `«term_⊴ᵣ_»`, `«term_⊵ᵣ_»`, `«termρᵣ[_]»`, `MonoidalRightActionStruct`, `actionAssocIso`, `actionHom`, `actionHomLeft`, `actionHomRight`, `actionObj`, `actionUnitIso`, `selRightfAction`, `selfLeftAction`	44
Theorems `actionAssocIso_hom_naturality`, `actionAssocIso_hom_naturality_assoc`, `actionAssocIso_inv_naturality`, `actionAssocIso_inv_naturality_assoc`, `actionAssocNatIso_hom_app_app_app`, `actionAssocNatIso_inv_app_app_app`, `actionHomLeft_action`, `actionHomLeft_action_assoc`, `actionHomRight_comp`, `actionHomRight_comp_assoc`, `actionHomRight_hom_inv`, `actionHomRight_hom_inv'`, `actionHomRight_hom_inv'_assoc`, `actionHomRight_hom_inv_assoc`, `actionHomRight_id`, `actionHomRight_id_assoc`, `actionHomRight_inv_hom`, `actionHomRight_inv_hom'`, `actionHomRight_inv_hom'_assoc`, `actionHomRight_inv_hom_assoc`, `actionHom_comp`, `actionHom_comp_assoc`, `actionHom_def`, `actionHom_def'`, `actionHom_def'_assoc`, `actionHom_def_assoc`, `actionHom_id`, `actionLeft_map`, `actionLeft_obj`, `actionRight_map`, `actionRight_obj`, `actionUnitIso_hom_naturality`, `actionUnitIso_hom_naturality_assoc`, `actionUnitIso_inv_naturality`, `actionUnitIso_inv_naturality_assoc`, `actionUnitNatIso_hom_app`, `actionUnitNatIso_inv_app`, `action_exchange`, `action_exchange_assoc`, `associator_actionHom`, `associator_actionHom_assoc`, `comp_actionHomLeft`, `comp_actionHomLeft_assoc`, `curriedAction_map_app`, `curriedAction_obj_map`, `curriedAction_obj_obj`, `hom_inv_actionHomLeft`, `hom_inv_actionHomLeft'`, `hom_inv_actionHomLeft'_assoc`, `hom_inv_actionHomLeft_assoc`, `id_actionHom`, `id_actionHomLeft`, `id_actionHomLeft_assoc`, `inv_actionHom`, `inv_actionHomLeft`, `inv_actionHomRight`, `inv_hom_actionHomLeft`, `inv_hom_actionHomLeft'`, `inv_hom_actionHomLeft'_assoc`, `inv_hom_actionHomLeft_assoc`, `isIso_actionHom`, `isIso_actionHomLeft`, `isIso_actionHomRight`, `leftUnitor_actionHom`, `leftUnitor_actionHom_assoc`, `rightUnitor_actionHom`, `rightUnitor_actionHom_assoc`, `tensor_actionHomRight`, `tensor_actionHomRight_assoc`, `unit_actionHomRight`, `unit_actionHomRight_assoc`, `whiskerLeft_actionHomLeft`, `whiskerLeft_actionHomLeft_assoc`, `whiskerRight_actionHomLeft`, `actionAssocIso_hom_naturality`, `actionAssocIso_hom_naturality_assoc`, `actionAssocIso_inv_naturality`, `actionAssocIso_inv_naturality_assoc`, `actionAssocNatIso_hom_app_app_app`, `actionAssocNatIso_inv_app_app_app`, `actionHomLeft_tensor`, `actionHomLeft_tensor_assoc`, `actionHomRight_comp`, `actionHomRight_comp_assoc`, `actionHomRight_hom_inv`, `actionHomRight_hom_inv'`, `actionHomRight_hom_inv'_assoc`, `actionHomRight_hom_inv_assoc`, `actionHomRight_id`, `actionHomRight_id_assoc`, `actionHomRight_inv_hom`, `actionHomRight_inv_hom'`, `actionHomRight_inv_hom'_assoc`, `actionHomRight_inv_hom_assoc`, `actionHomRight_whiskerRight`, `actionHomRight_whiskerRight_assoc`, `actionHom_associator`, `actionHom_associator_assoc`, `actionHom_comp`, `actionHom_comp_assoc`, `actionHom_def`, `actionHom_def'`, `actionHom_def'_assoc`, `actionHom_def_assoc`, `actionHom_id`, `actionHom_leftUnitor`, `actionHom_leftUnitor_assoc`, `actionHom_rightUnitor`, `actionHom_rightUnitor_assoc`, `actionLeft_map`, `actionLeft_obj`, `actionRight_map`, `actionRight_obj`, `actionUnitIso_hom_naturality`, `actionUnitIso_hom_naturality_assoc`, `actionUnitIso_inv_naturality`, `actionUnitIso_inv_naturality_assoc`, `actionUnitNatIso_hom_app`, `actionUnitNatIso_inv_app`, `action_actionHomRight`, `action_actionHomRight_assoc`, `action_exchange`, `action_exchange_assoc`, `comp_actionHomLeft`, `comp_actionHomLeft_assoc`, `curriedAction_map_app`, `curriedAction_obj_map`, `curriedAction_obj_obj`, `hom_inv_actionHomLeft`, `hom_inv_actionHomLeft'`, `hom_inv_actionHomLeft'_assoc`, `hom_inv_actionHomLeft_assoc`, `id_actionHom`, `id_actionHomLeft`, `id_actionHomLeft_assoc`, `inv_actionHom`, `inv_actionHomLeft`, `inv_actionHomRight`, `inv_hom_actionHomLeft`, `inv_hom_actionHomLeft'`, `inv_hom_actionHomLeft'_assoc`, `inv_hom_actionHomLeft_assoc`, `isIso_actionHom`, `isIso_actionHomLeft`, `isIso_actionHomRight`, `unit_actionHomRight`, `unit_actionHomRight_assoc`, `whiskerRight_actionHomLeft`, `selRightfAction_actionAssocIso_hom`, `selRightfAction_actionAssocIso_inv`, `selRightfAction_actionHom`, `selRightfAction_actionHomLeft`, `selRightfAction_actionHomRight`, `selRightfAction_actionObj`, `selRightfAction_actionUnitIso`, `selfLeftAction_actionAssocIso`, `selfLeftAction_actionHom`, `selfLeftAction_actionHomLeft`, `selfLeftAction_actionHomRight`, `selfLeftAction_actionObj`, `selfLeftAction_actionUnitIso`	161
Total	205

CategoryTheory.MonoidalCategory

Definitions

Name	Category	Theorems
`MonoidalLeftAction` 📖	CompData	—
`MonoidalLeftActionStruct` 📖	CompData	—
`MonoidalRightAction` 📖	CompData	—
`MonoidalRightActionStruct` 📖	CompData	—
`selRightfAction` 📖	CompOp	7 math math: `selRightfAction_actionHomRight`, `selRightfAction_actionHom`, `selRightfAction_actionUnitIso`, `selRightfAction_actionHomLeft`, `selRightfAction_actionAssocIso_hom`, `selRightfAction_actionAssocIso_inv`, `selRightfAction_actionObj`
`selfLeftAction` 📖	CompOp	12 math math: `selfLeftAction_actionUnitIso`, `selfLeftAction_actionHomLeft`, `selfLeftAction_actionHom`, `CategoryTheory.ModObj.smul_eq_mul`, `selfLeftAction_actionObj`, `CategoryTheory.ModObj.ext_iff`, `CategoryTheory.Mod_.trivialAction_X`, `CategoryTheory.Mod_.regular_mod_smul`, `selfLeftAction_actionAssocIso`, `CategoryTheory.Mod_.regular_X`, `CategoryTheory.Mod_.trivialAction_mod_smul`, `selfLeftAction_actionHomRight`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`selRightfAction_actionAssocIso_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `toMonoidalCategoryStruct` `MonoidalRightActionStruct.actionAssocIso` `MonoidalRightAction.toMonoidalRightActionStruct` `selRightfAction` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategoryStruct.associator`	—	—
`selRightfAction_actionAssocIso_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `toMonoidalCategoryStruct` `MonoidalRightActionStruct.actionAssocIso` `MonoidalRightAction.toMonoidalRightActionStruct` `selRightfAction` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.associator`	—	—
`selRightfAction_actionHom` 📖	mathematical	—	`MonoidalRightActionStruct.actionHom` `toMonoidalCategoryStruct` `MonoidalRightAction.toMonoidalRightActionStruct` `selRightfAction` `CategoryTheory.MonoidalCategoryStruct.tensorHom`	—	—
`selRightfAction_actionHomLeft` 📖	mathematical	—	`MonoidalRightActionStruct.actionHomLeft` `toMonoidalCategoryStruct` `MonoidalRightAction.toMonoidalRightActionStruct` `selRightfAction` `CategoryTheory.MonoidalCategoryStruct.whiskerRight`	—	—
`selRightfAction_actionHomRight` 📖	mathematical	—	`MonoidalRightActionStruct.actionHomRight` `toMonoidalCategoryStruct` `MonoidalRightAction.toMonoidalRightActionStruct` `selRightfAction` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft`	—	—
`selRightfAction_actionObj` 📖	mathematical	—	`MonoidalRightActionStruct.actionObj` `toMonoidalCategoryStruct` `MonoidalRightAction.toMonoidalRightActionStruct` `selRightfAction` `CategoryTheory.MonoidalCategoryStruct.tensorObj`	—	—
`selRightfAction_actionUnitIso` 📖	mathematical	—	`MonoidalRightActionStruct.actionUnitIso` `toMonoidalCategoryStruct` `MonoidalRightAction.toMonoidalRightActionStruct` `selRightfAction` `CategoryTheory.MonoidalCategoryStruct.rightUnitor`	—	—
`selfLeftAction_actionAssocIso` 📖	mathematical	—	`MonoidalLeftActionStruct.actionAssocIso` `toMonoidalCategoryStruct` `MonoidalLeftAction.toMonoidalLeftActionStruct` `selfLeftAction` `CategoryTheory.MonoidalCategoryStruct.associator`	—	—
`selfLeftAction_actionHom` 📖	mathematical	—	`MonoidalLeftActionStruct.actionHom` `toMonoidalCategoryStruct` `MonoidalLeftAction.toMonoidalLeftActionStruct` `selfLeftAction` `CategoryTheory.MonoidalCategoryStruct.tensorHom`	—	—
`selfLeftAction_actionHomLeft` 📖	mathematical	—	`MonoidalLeftActionStruct.actionHomLeft` `toMonoidalCategoryStruct` `MonoidalLeftAction.toMonoidalLeftActionStruct` `selfLeftAction` `CategoryTheory.MonoidalCategoryStruct.whiskerRight`	—	—
`selfLeftAction_actionHomRight` 📖	mathematical	—	`MonoidalLeftActionStruct.actionHomRight` `toMonoidalCategoryStruct` `MonoidalLeftAction.toMonoidalLeftActionStruct` `selfLeftAction` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft`	—	—
`selfLeftAction_actionObj` 📖	mathematical	—	`MonoidalLeftActionStruct.actionObj` `toMonoidalCategoryStruct` `MonoidalLeftAction.toMonoidalLeftActionStruct` `selfLeftAction` `CategoryTheory.MonoidalCategoryStruct.tensorObj`	—	—
`selfLeftAction_actionUnitIso` 📖	mathematical	—	`MonoidalLeftActionStruct.actionUnitIso` `toMonoidalCategoryStruct` `MonoidalLeftAction.toMonoidalLeftActionStruct` `selfLeftAction` `CategoryTheory.MonoidalCategoryStruct.leftUnitor`	—	—

CategoryTheory.MonoidalCategory.MonoidalLeftAction

Definitions

Name	Category	Theorems
`actionAssocNatIso` 📖	CompOp	2 math math: `actionAssocNatIso_hom_app_app_app`, `actionAssocNatIso_inv_app_app_app`
`actionLeft` 📖	CompOp	6 math math: `actionUnitNatIso_inv_app`, `actionUnitNatIso_hom_app`, `actionLeft_map`, `curriedActionMopMonoidal_η_unmop_app`, `curriedActionMopMonoidal_ε_unmop_app`, `actionLeft_obj`
`actionRight` 📖	CompOp	2 math math: `actionRight_obj`, `actionRight_map`
`actionUnitNatIso` 📖	CompOp	2 math math: `actionUnitNatIso_inv_app`, `actionUnitNatIso_hom_app`
`curriedAction` 📖	CompOp	9 math math: `actionAssocNatIso_hom_app_app_app`, `curriedActionMopMonoidal_μ_unmop_app`, `actionAssocNatIso_inv_app_app_app`, `curriedAction_map_app`, `curriedActionMopMonoidal_δ_unmop_app`, `curriedActionMopMonoidal_η_unmop_app`, `curriedActionMopMonoidal_ε_unmop_app`, `curriedAction_obj_obj`, `curriedAction_obj_map`
`termαₗ` 📖	CompOp	—
`toMonoidalLeftActionStruct` 📖	CompOp	197 math math: `actionUnitNatIso_inv_app`, `CategoryTheory.ModObj.one_smul_assoc`, `actionHomRight_hom_inv_assoc`, `actionOfMonoidalFunctorToEndofunctorMop_actionHomLeft`, `actionOfMonoidalFunctorToEndofunctorMop_actionAssocIso_hom`, `actionUnitNatIso_hom_app`, `CategoryTheory.ModObj.mul_smul_assoc`, `actionLeft_map`, `leftActionOfMonoidalOppositeRightAction_actionObj`, `oppositeLeftAction_actionHomRight`, `oppositeLeftAction_actionAssocIso`, `CategoryTheory.Functor.LaxLeftLinear.μₗ_naturality_right`, `leftActionOfOppositeLeftAction_actionHomRight`, `CategoryTheory.MonoidalCategory.selfLeftAction_actionUnitIso`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionHomLeft`, `isIso_actionHom`, `CategoryTheory.Functor.LeftLinear.instIsIsoδₗ`, `CategoryTheory.MonoidalCategory.selfLeftAction_actionHomLeft`, `CategoryTheory.Functor.OplaxLeftLinear.δₗ_associativity_inv`, `leftActionOfOppositeLeftAction_actionAssocIso`, `leftUnitor_actionHom_assoc`, `action_exchange`, `leftActionOfMonoidalOppositeRightAction_actionHom`, `actionAssocNatIso_hom_app_app_app`, `actionHomRight_id_assoc`, `actionHomLeft_action_assoc`, `monoidalOppositeLeftAction_actionHomLeft`, `actionHomRight_hom_inv`, `curriedActionMopMonoidal_μ_unmop_app`, `isIso_actionHomLeft`, `actionHomLeft_action`, `CategoryTheory.ModObj.mul_smul'_assoc`, `actionHom_def_assoc`, `actionUnitIso_hom_naturality_assoc`, `CategoryTheory.Functor.LeftLinear.μₗ_comp_δₗ_assoc`, `actionAssocIso_inv_naturality_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction_actionHom`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionAssocIso_mop_mop`, `monoidalOppositeLeftAction_actionHomRight`, `CategoryTheory.Functor.LaxLeftLinear.μₗ_associativity_inv_assoc`, `actionHom_comp_assoc`, `CategoryTheory.Functor.LeftLinear.inv_μₗ`, `actionHomRight_inv_hom_assoc`, `CategoryTheory.IsMod_Hom.smul_hom`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionHom`, `CategoryTheory.Functor.LaxLeftLinear.μₗ_naturality_right_assoc`, `CategoryTheory.MonoidalCategory.selfLeftAction_actionHom`, `CategoryTheory.Functor.OplaxLeftLinear.δₗ_naturality_left_assoc`, `id_actionHomLeft`, `inv_actionHomLeft`, `whiskerLeft_actionHomLeft_assoc`, `action_exchange_assoc`, `id_actionHom`, `CategoryTheory.Functor.OplaxLeftLinear.δₗ_unitality_hom_assoc`, `tensor_actionHomRight`, `CategoryTheory.ModObj.one_smul'_assoc`, `rightUnitor_actionHom`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionHomRight_mop`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionAssocIso`, `leftActionOfOppositeLeftAction_actionObj`, `CategoryTheory.Functor.OplaxLeftLinear.δₗ_unitality_inv`, `leftActionOfOppositeLeftAction_actionHom_unop`, `monoidalOppositeLeftAction_actionHomLeft_mop`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction_actionObj`, `CategoryTheory.Functor.OplaxLeftLinear.δₗ_associativity`, `monoidalOppositeLeftAction_actionUnitIso`, `CategoryTheory.Functor.LeftLinear.δₗ_comp_μₗ`, `hom_inv_actionHomLeft'_assoc`, `monoidalOppositeLeftAction_actionHom_mop_mop`, `CategoryTheory.Functor.LaxLeftLinear.μₗ_unitality_assoc`, `leftActionOfMonoidalOppositeRightAction_actionAssocIso`, `actionAssocNatIso_inv_app_app_app`, `CategoryTheory.IsMod_Hom.smul_hom_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionHomRight`, `actionHomRight_id`, `id_actionHomLeft_assoc`, `actionAssocIso_hom_naturality`, `oppositeLeftAction_actionHomLeft_op`, `unit_actionHomRight_assoc`, `curriedAction_map_app`, `leftUnitor_actionHom`, `actionHomRight_inv_hom'_assoc`, `leftActionOfOppositeLeftAction_actionUnitIso`, `actionHomRight_inv_hom'`, `associator_actionHom_assoc`, `leftActionOfOppositeLeftAction_actionHomLeft_unop`, `oppositeLeftAction_actionObj`, `leftActionOfMonoidalOppositeRightAction_actionUnitIso`, `actionRight_obj`, `monoidalOppositeLeftAction_actionAssocIso`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction_actionHomLeft`, `hom_inv_actionHomLeft_assoc`, `CategoryTheory.ModObj.one_smul'`, `actionHom_id`, `actionHomRight_inv_hom`, `tensor_actionHomRight_assoc`, `actionOfMonoidalFunctorToEndofunctorMop_actionObj`, `CategoryTheory.Functor.LaxLeftLinear.μₗ_associativity`, `actionHomRight_comp_assoc`, `rightUnitor_actionHom_assoc`, `actionHomRight_hom_inv'_assoc`, `CategoryTheory.Functor.OplaxLeftLinear.δₗ_unitality_hom`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction_actionUnitIso`, `leftActionOfOppositeLeftAction_actionAssocIso_unop`, `whiskerLeft_actionHomLeft`, `CategoryTheory.Functor.LaxLeftLinear.μₗ_naturality_left`, `actionAssocIso_hom_naturality_assoc`, `leftActionOfMonoidalOppositeRightAction_actionHomLeft`, `curriedActionMop_map_unmop_app`, `actionHomRight_comp`, `CategoryTheory.ModObj.assoc_flip`, `actionHomRight_hom_inv'`, `curriedActionMopMonoidal_δ_unmop_app`, `CategoryTheory.MonoidalCategory.selfLeftAction_actionObj`, `CategoryTheory.Functor.OplaxLeftLinear.δₗ_naturality_right`, `CategoryTheory.Functor.OplaxLeftLinear.δₗ_associativity_assoc`, `oppositeLeftAction_actionRight_op`, `inv_actionHomRight`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionObj_mop`, `CategoryTheory.Functor.LaxLeftLinear.μₗ_associativity_inv`, `unit_actionHomRight`, `CategoryTheory.Functor.LaxLeftLinear.μₗ_unitality_inv`, `oppositeLeftAction_actionHom_op`, `curriedActionMop_obj_unmop_obj`, `CategoryTheory.ModObj.one_smul`, `leftActionOfOppositeLeftAction_actionRight_unop`, `actionUnitIso_inv_naturality_assoc`, `CategoryTheory.Functor.LaxLeftLinear.μₗ_unitality`, `whiskerRight_actionHomLeft`, `leftActionOfOppositeLeftAction_actionObj_unop`, `oppositeLeftAction_actionHom`, `monoidalOppositeLeftAction_actionObj`, `CategoryTheory.Functor.LaxLeftLinear.μₗ_unitality_inv_assoc`, `CategoryTheory.Functor.OplaxLeftLinear.δₗ_unitality_inv_assoc`, `monoidalOppositeLeftAction_actionObj_mop`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionHom_mop_mop`, `comp_actionHomLeft`, `actionOfMonoidalFunctorToEndofunctorMop_actionHomRight`, `comp_actionHomLeft_assoc`, `monoidalOppositeLeftAction_actionHom`, `CategoryTheory.Functor.OplaxLeftLinear.δₗ_naturality_left`, `CategoryTheory.Mod_.scalarRestriction_smul`, `actionAssocIso_inv_naturality`, `leftActionOfOppositeLeftAction_actionHom`, `inv_hom_actionHomLeft'_assoc`, `CategoryTheory.Functor.LaxLeftLinear.μₗ_naturality_left_assoc`, `actionUnitIso_hom_naturality`, `CategoryTheory.ModObj.smul_def`, `oppositeLeftAction_actionAssocIso_op`, `actionOfMonoidalFunctorToEndofunctorMop_actionUnitIso_hom`, `monoidalOppositeLeftAction_actionRight_mop`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction_actionHomRight`, `actionHom_def`, `actionHom_def'`, `actionOfMonoidalFunctorToEndofunctorMop_actionUnitIso_inv`, `CategoryTheory.Functor.OplaxLeftLinear.δₗ_naturality_right_assoc`, `CategoryTheory.Functor.LeftLinear.inv_δₗ`, `curriedActionMop_obj_unmop_map`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionObj`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction_actionAssocIso`, `inv_actionHom`, `CategoryTheory.Functor.LeftLinear.μₗ_comp_δₗ`, `CategoryTheory.Mod_.assoc_flip`, `oppositeLeftAction_actionHomLeft`, `associator_actionHom`, `CategoryTheory.Functor.LeftLinear.instIsIsoμₗ`, `CategoryTheory.MonoidalCategory.selfLeftAction_actionAssocIso`, `CategoryTheory.Functor.LaxLeftLinear.μₗ_associativity_assoc`, `actionOfMonoidalFunctorToEndofunctorMop_actionAssocIso_inv`, `actionRight_map`, `curriedActionMopMonoidal_η_unmop_app`, `CategoryTheory.ModObj.mul_smul`, `leftActionOfMonoidalOppositeRightAction_actionHomRight`, `curriedActionMopMonoidal_ε_unmop_app`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionRight_mop`, `inv_hom_actionHomLeft_assoc`, `CategoryTheory.ModObj.mul_smul'`, `actionLeft_obj`, `monoidalOppositeLeftAction_actionAssocIso_mop_mop`, `hom_inv_actionHomLeft`, `hom_inv_actionHomLeft'`, `CategoryTheory.MonoidalCategory.selfLeftAction_actionHomRight`, `actionOfMonoidalFunctorToEndofunctorMop_actionHom`, `oppositeLeftAction_actionObj_op`, `actionUnitIso_inv_naturality`, `oppositeLeftAction_actionUnitIso`, `CategoryTheory.Functor.LeftLinear.δₗ_comp_μₗ_assoc`, `leftActionOfOppositeLeftAction_actionHomLeft`, `actionHom_comp`, `inv_hom_actionHomLeft`, `curriedAction_obj_obj`, `CategoryTheory.Functor.OplaxLeftLinear.δₗ_associativity_inv_assoc`, `curriedAction_obj_map`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionUnitIso`, `inv_hom_actionHomLeft'`, `isIso_actionHomRight`, `actionHom_def'_assoc`
`«term_⊙ₗ_»` 📖	CompOp	—
`«term_⊙ₗₘ_»` 📖	CompOp	—
`«term_⊴ₗ_»` 📖	CompOp	—
`«term_⊵ₗ_»` 📖	CompOp	—
`«termλₗ[_]»` 📖	CompOp	—
`«termλₗ»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`actionAssocIso_hom_naturality` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom` `CategoryTheory.MonoidalCategoryStruct.tensorHom` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso`	—	—
`actionAssocIso_hom_naturality_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom` `CategoryTheory.MonoidalCategoryStruct.tensorHom` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `actionAssocIso_hom_naturality`
`actionAssocIso_inv_naturality` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso` `CategoryTheory.MonoidalCategoryStruct.tensorHom`	—	`CategoryTheory.Iso.comp_inv_eq` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.inv_comp_eq` `actionAssocIso_hom_naturality`
`actionAssocIso_inv_naturality_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso` `CategoryTheory.MonoidalCategoryStruct.tensorHom`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `actionAssocIso_inv_naturality`
`actionAssocNatIso_hom_app_app_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.bifunctorComp₁₂` `CategoryTheory.MonoidalCategory.curriedTensor` `curriedAction` `CategoryTheory.bifunctorComp₂₃` `CategoryTheory.Iso.hom` `actionAssocNatIso` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso`	—	—
`actionAssocNatIso_inv_app_app_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.bifunctorComp₂₃` `curriedAction` `CategoryTheory.bifunctorComp₁₂` `CategoryTheory.MonoidalCategory.curriedTensor` `CategoryTheory.Iso.inv` `actionAssocNatIso` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso`	—	—
`actionHomLeft_action` 📖	mathematical	—	`CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso` `CategoryTheory.MonoidalCategoryStruct.whiskerRight` `CategoryTheory.Iso.hom`	—	`whiskerRight_actionHomLeft` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.inv_hom_id` `CategoryTheory.Category.comp_id` `CategoryTheory.Iso.inv_hom_id_assoc`
`actionHomLeft_action_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso` `CategoryTheory.MonoidalCategoryStruct.whiskerRight` `CategoryTheory.Iso.hom`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `actionHomLeft_action`
`actionHomRight_comp` 📖	mathematical	—	`CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj`	—	`CategoryTheory.Category.comp_id`
`actionHomRight_comp_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `actionHomRight_comp`
`actionHomRight_hom_inv` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight` `CategoryTheory.Iso.hom` `CategoryTheory.Iso.inv` `CategoryTheory.CategoryStruct.id`	—	`actionHomRight_comp` `CategoryTheory.Iso.hom_inv_id` `actionHomRight_id`
`actionHomRight_hom_inv'` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight` `CategoryTheory.inv` `CategoryTheory.CategoryStruct.id`	—	`actionHomRight_comp` `CategoryTheory.IsIso.hom_inv_id` `actionHomRight_id`
`actionHomRight_hom_inv'_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight` `CategoryTheory.inv`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Category.id_comp` `Mathlib.Tactic.Reassoc.eq_whisker'` `actionHomRight_hom_inv'`
`actionHomRight_hom_inv_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight` `CategoryTheory.Iso.hom` `CategoryTheory.Iso.inv`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Category.id_comp` `Mathlib.Tactic.Reassoc.eq_whisker'` `actionHomRight_hom_inv`
`actionHomRight_id` 📖	mathematical	—	`CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj`	—	—
`actionHomRight_id_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight` `CategoryTheory.CategoryStruct.id`	—	`CategoryTheory.Category.id_comp` `Mathlib.Tactic.Reassoc.eq_whisker'` `actionHomRight_id`
`actionHomRight_inv_hom` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight` `CategoryTheory.Iso.inv` `CategoryTheory.Iso.hom` `CategoryTheory.CategoryStruct.id`	—	`actionHomRight_comp` `CategoryTheory.Iso.inv_hom_id` `actionHomRight_id`
`actionHomRight_inv_hom'` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight` `CategoryTheory.inv` `CategoryTheory.CategoryStruct.id`	—	`actionHomRight_comp` `CategoryTheory.IsIso.inv_hom_id` `actionHomRight_id`
`actionHomRight_inv_hom'_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight` `CategoryTheory.inv`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Category.id_comp` `Mathlib.Tactic.Reassoc.eq_whisker'` `actionHomRight_inv_hom'`
`actionHomRight_inv_hom_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight` `CategoryTheory.Iso.inv` `CategoryTheory.Iso.hom`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Category.id_comp` `Mathlib.Tactic.Reassoc.eq_whisker'` `actionHomRight_inv_hom`
`actionHom_comp` 📖	mathematical	—	`CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj`	—	—
`actionHom_comp_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `actionHom_comp`
`actionHom_def` 📖	mathematical	—	`CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight`	—	—
`actionHom_def'` 📖	mathematical	—	`CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft`	—	`actionHom_def` `action_exchange`
`actionHom_def'_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `actionHom_def'`
`actionHom_def_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `actionHom_def`
`actionHom_id` 📖	mathematical	—	`CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft`	—	`actionHom_def` `actionHomRight_id` `CategoryTheory.Category.comp_id`
`actionLeft_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `actionLeft` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct`	—	—
`actionLeft_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `actionLeft` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct`	—	—
`actionRight_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `actionRight` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct`	—	—
`actionRight_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `actionRight` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct`	—	—
`actionUnitIso_hom_naturality` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight`	—	—
`actionUnitIso_hom_naturality_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `actionUnitIso_hom_naturality`
`actionUnitIso_inv_naturality` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight`	—	`CategoryTheory.Iso.inv_comp_eq` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.comp_inv_eq` `actionUnitIso_hom_naturality`
`actionUnitIso_inv_naturality_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `actionUnitIso_inv_naturality`
`actionUnitNatIso_hom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `actionLeft` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Functor.id` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `actionUnitNatIso` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso`	—	—
`actionUnitNatIso_inv_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.id` `actionLeft` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `actionUnitNatIso` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso`	—	—
`action_exchange` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft`	—	`CategoryTheory.Category.id_comp` `CategoryTheory.Category.comp_id`
`action_exchange_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `action_exchange`
`associator_actionHom` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.associator` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight`	—	—
`associator_actionHom_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.associator` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `associator_actionHom`
`comp_actionHomLeft` 📖	mathematical	—	`CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj`	—	`CategoryTheory.Category.id_comp`
`comp_actionHomLeft_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `comp_actionHomLeft`
`curriedAction_map_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight` `CategoryTheory.Functor.map` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `curriedAction` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft`	—	—
`curriedAction_obj_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `curriedAction` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct`	—	—
`curriedAction_obj_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `curriedAction` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct`	—	—
`hom_inv_actionHomLeft` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft` `CategoryTheory.Iso.hom` `CategoryTheory.Iso.inv` `CategoryTheory.CategoryStruct.id`	—	`comp_actionHomLeft` `CategoryTheory.Iso.hom_inv_id` `id_actionHomLeft`
`hom_inv_actionHomLeft'` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft` `CategoryTheory.inv` `CategoryTheory.CategoryStruct.id`	—	`comp_actionHomLeft` `CategoryTheory.IsIso.hom_inv_id` `id_actionHomLeft`
`hom_inv_actionHomLeft'_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft` `CategoryTheory.inv`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Category.id_comp` `Mathlib.Tactic.Reassoc.eq_whisker'` `hom_inv_actionHomLeft'`
`hom_inv_actionHomLeft_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft` `CategoryTheory.Iso.hom` `CategoryTheory.Iso.inv`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Category.id_comp` `Mathlib.Tactic.Reassoc.eq_whisker'` `hom_inv_actionHomLeft`
`id_actionHom` 📖	mathematical	—	`CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight`	—	`actionHom_def` `id_actionHomLeft` `CategoryTheory.Category.id_comp`
`id_actionHomLeft` 📖	mathematical	—	`CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj`	—	—
`id_actionHomLeft_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft` `CategoryTheory.CategoryStruct.id`	—	`CategoryTheory.Category.id_comp` `Mathlib.Tactic.Reassoc.eq_whisker'` `id_actionHomLeft`
`inv_actionHom` 📖	mathematical	—	`CategoryTheory.inv` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom` `isIso_actionHom`	—	`CategoryTheory.IsIso.inv_eq_of_hom_inv_id` `isIso_actionHom` `CategoryTheory.IsIso.hom_inv_id` `actionHom_id` `id_actionHomLeft`
`inv_actionHomLeft` 📖	mathematical	—	`CategoryTheory.inv` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft` `isIso_actionHomLeft`	—	`CategoryTheory.IsIso.inv_eq_of_hom_inv_id` `isIso_actionHomLeft` `hom_inv_actionHomLeft'`
`inv_actionHomRight` 📖	mathematical	—	`CategoryTheory.inv` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight` `isIso_actionHomRight`	—	`CategoryTheory.IsIso.inv_eq_of_hom_inv_id` `isIso_actionHomRight` `actionHomRight_hom_inv'`
`inv_hom_actionHomLeft` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft` `CategoryTheory.Iso.inv` `CategoryTheory.Iso.hom` `CategoryTheory.CategoryStruct.id`	—	`comp_actionHomLeft` `CategoryTheory.Iso.inv_hom_id` `id_actionHomLeft`
`inv_hom_actionHomLeft'` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft` `CategoryTheory.inv` `CategoryTheory.CategoryStruct.id`	—	`comp_actionHomLeft` `CategoryTheory.IsIso.inv_hom_id` `id_actionHomLeft`
`inv_hom_actionHomLeft'_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft` `CategoryTheory.inv`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Category.id_comp` `Mathlib.Tactic.Reassoc.eq_whisker'` `inv_hom_actionHomLeft'`
`inv_hom_actionHomLeft_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft` `CategoryTheory.Iso.inv` `CategoryTheory.Iso.hom`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Category.id_comp` `Mathlib.Tactic.Reassoc.eq_whisker'` `inv_hom_actionHomLeft`
`isIso_actionHom` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom`	—	`CategoryTheory.IsIso.hom_inv_id` `actionHom_id` `id_actionHomLeft` `CategoryTheory.IsIso.inv_hom_id`
`isIso_actionHomLeft` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft`	—	`hom_inv_actionHomLeft'` `inv_hom_actionHomLeft'`
`isIso_actionHomRight` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight`	—	`actionHomRight_hom_inv'` `actionHomRight_inv_hom'`
`leftUnitor_actionHom` 📖	mathematical	—	`CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.leftUnitor` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso`	—	—
`leftUnitor_actionHom_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.leftUnitor` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `leftUnitor_actionHom`
`rightUnitor_actionHom` 📖	mathematical	—	`CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.rightUnitor` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso`	—	—
`rightUnitor_actionHom_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.rightUnitor` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `rightUnitor_actionHom`
`tensor_actionHomRight` 📖	mathematical	—	`CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso` `CategoryTheory.Iso.inv`	—	`CategoryTheory.Category.assoc` `actionAssocIso_hom_naturality` `id_actionHom` `CategoryTheory.MonoidalCategory.tensorHom_id` `CategoryTheory.MonoidalCategory.id_whiskerRight` `CategoryTheory.Iso.hom_inv_id` `CategoryTheory.Category.comp_id`
`tensor_actionHomRight_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso` `CategoryTheory.Iso.inv`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `tensor_actionHomRight`
`unit_actionHomRight` 📖	mathematical	—	`CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso` `CategoryTheory.Iso.inv`	—	`CategoryTheory.Category.assoc` `actionUnitIso_hom_naturality` `CategoryTheory.Iso.hom_inv_id` `CategoryTheory.Category.comp_id`
`unit_actionHomRight_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso` `CategoryTheory.Iso.inv`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `unit_actionHomRight`
`whiskerLeft_actionHomLeft` 📖	mathematical	—	`CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight` `CategoryTheory.Iso.inv`	—	—
`whiskerLeft_actionHomLeft_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight` `CategoryTheory.Iso.inv`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `whiskerLeft_actionHomLeft`
`whiskerRight_actionHomLeft` 📖	mathematical	—	`CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategoryStruct.whiskerRight` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso` `CategoryTheory.Iso.inv`	—	—

CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct

Definitions

Name	Category	Theorems
`actionAssocIso` 📖	CompOp	48 math math: `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionAssocIso_hom`, `CategoryTheory.ModObj.mul_smul_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_actionAssocIso`, `CategoryTheory.Functor.OplaxLeftLinear.δₗ_associativity_inv`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_actionAssocIso`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftUnitor_actionHom_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionAssocNatIso_hom_app_app_app`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomLeft_action_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMopMonoidal_μ_unmop_app`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomLeft_action`, `CategoryTheory.ModObj.mul_smul'_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionAssocIso_inv_naturality_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionAssocIso_mop_mop`, `CategoryTheory.Functor.LaxLeftLinear.μₗ_associativity_inv_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.whiskerLeft_actionHomLeft_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.tensor_actionHomRight`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.rightUnitor_actionHom`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionAssocIso`, `CategoryTheory.Functor.OplaxLeftLinear.δₗ_associativity`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction_actionAssocIso`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionAssocNatIso_inv_app_app_app`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionAssocIso_hom_naturality`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftUnitor_actionHom`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.associator_actionHom_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionAssocIso`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.tensor_actionHomRight_assoc`, `CategoryTheory.Functor.LaxLeftLinear.μₗ_associativity`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.rightUnitor_actionHom_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_actionAssocIso_unop`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.whiskerLeft_actionHomLeft`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionAssocIso_hom_naturality_assoc`, `CategoryTheory.ModObj.assoc_flip`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMopMonoidal_δ_unmop_app`, `CategoryTheory.Functor.OplaxLeftLinear.δₗ_associativity_assoc`, `CategoryTheory.Functor.LaxLeftLinear.μₗ_associativity_inv`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.whiskerRight_actionHomLeft`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionAssocIso_inv_naturality`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_actionAssocIso_op`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction_actionAssocIso`, `CategoryTheory.Mod_.assoc_flip`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.associator_actionHom`, `CategoryTheory.MonoidalCategory.selfLeftAction_actionAssocIso`, `CategoryTheory.Functor.LaxLeftLinear.μₗ_associativity_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionAssocIso_inv`, `CategoryTheory.ModObj.mul_smul`, `CategoryTheory.ModObj.mul_smul'`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionAssocIso_mop_mop`, `CategoryTheory.Functor.OplaxLeftLinear.δₗ_associativity_inv_assoc`
`actionHom` 📖	CompOp	26 math math: `CategoryTheory.MonoidalCategory.MonoidalLeftAction.isIso_actionHom`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction_actionHom`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_def_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionAssocIso_inv_naturality_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction_actionHom`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_comp_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionHom`, `CategoryTheory.MonoidalCategory.selfLeftAction_actionHom`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.id_actionHom`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_actionHom_unop`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionHom_mop_mop`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionAssocIso_hom_naturality`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_id`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionAssocIso_hom_naturality_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_actionHom_op`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_actionHom`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionHom_mop_mop`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionHom`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionAssocIso_inv_naturality`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_actionHom`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_def`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_def'`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.inv_actionHom`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionHom`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_comp`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_def'_assoc`
`actionHomLeft` 📖	CompOp	62 math math: `CategoryTheory.ModObj.one_smul_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionHomLeft`, `CategoryTheory.ModObj.mul_smul_assoc`, `CategoryTheory.MonoidalCategory.selfLeftAction_actionHomLeft`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftUnitor_actionHom_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.action_exchange`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomLeft_action_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionHomLeft`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.isIso_actionHomLeft`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomLeft_action`, `CategoryTheory.ModObj.mul_smul'_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_def_assoc`, `CategoryTheory.Functor.OplaxLeftLinear.δₗ_naturality_left_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.id_actionHomLeft`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.inv_actionHomLeft`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.whiskerLeft_actionHomLeft_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.action_exchange_assoc`, `CategoryTheory.ModObj.one_smul'_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.rightUnitor_actionHom`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionHomRight_mop`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionHomLeft_mop`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.hom_inv_actionHomLeft'_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionHomRight`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.id_actionHomLeft_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_actionHomLeft_op`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedAction_map_app`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftUnitor_actionHom`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.associator_actionHom_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_actionHomLeft_unop`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.hom_inv_actionHomLeft_assoc`, `CategoryTheory.ModObj.one_smul'`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_id`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.rightUnitor_actionHom_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.whiskerLeft_actionHomLeft`, `CategoryTheory.Functor.LaxLeftLinear.μₗ_naturality_left`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction_actionHomLeft`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMop_map_unmop_app`, `CategoryTheory.ModObj.assoc_flip`, `CategoryTheory.ModObj.one_smul`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.whiskerRight_actionHomLeft`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.comp_actionHomLeft`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.comp_actionHomLeft_assoc`, `CategoryTheory.Functor.OplaxLeftLinear.δₗ_naturality_left`, `CategoryTheory.Mod_.scalarRestriction_smul`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.inv_hom_actionHomLeft'_assoc`, `CategoryTheory.Functor.LaxLeftLinear.μₗ_naturality_left_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction_actionHomRight`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_def`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_def'`, `CategoryTheory.Mod_.assoc_flip`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_actionHomLeft`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.associator_actionHom`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionRight_map`, `CategoryTheory.ModObj.mul_smul`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.inv_hom_actionHomLeft_assoc`, `CategoryTheory.ModObj.mul_smul'`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.hom_inv_actionHomLeft`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.hom_inv_actionHomLeft'`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_actionHomLeft`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.inv_hom_actionHomLeft`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.inv_hom_actionHomLeft'`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_def'_assoc`
`actionHomRight` 📖	CompOp	71 math math: `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_hom_inv_assoc`, `CategoryTheory.ModObj.mul_smul_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionLeft_map`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_actionHomRight`, `CategoryTheory.Functor.LaxLeftLinear.μₗ_naturality_right`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_actionHomRight`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionHomLeft`, `CategoryTheory.Functor.OplaxLeftLinear.δₗ_associativity_inv`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.action_exchange`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_id_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_hom_inv`, `CategoryTheory.ModObj.mul_smul'_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_def_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionUnitIso_hom_naturality_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionHomRight`, `CategoryTheory.Functor.LaxLeftLinear.μₗ_associativity_inv_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_inv_hom_assoc`, `CategoryTheory.IsMod_Hom.smul_hom`, `CategoryTheory.Functor.LaxLeftLinear.μₗ_naturality_right_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.whiskerLeft_actionHomLeft_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.action_exchange_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.id_actionHom`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.tensor_actionHomRight`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.rightUnitor_actionHom`, `CategoryTheory.Functor.OplaxLeftLinear.δₗ_associativity`, `CategoryTheory.IsMod_Hom.smul_hom_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_id`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.unit_actionHomRight_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedAction_map_app`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_inv_hom'_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_inv_hom'`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.associator_actionHom_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction_actionHomLeft`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_inv_hom`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.tensor_actionHomRight_assoc`, `CategoryTheory.Functor.LaxLeftLinear.μₗ_associativity`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_comp_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.rightUnitor_actionHom_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_hom_inv'_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.whiskerLeft_actionHomLeft`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_comp`, `CategoryTheory.ModObj.assoc_flip`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_hom_inv'`, `CategoryTheory.Functor.OplaxLeftLinear.δₗ_naturality_right`, `CategoryTheory.Functor.OplaxLeftLinear.δₗ_associativity_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_actionRight_op`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.inv_actionHomRight`, `CategoryTheory.Functor.LaxLeftLinear.μₗ_associativity_inv`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.unit_actionHomRight`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_actionRight_unop`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionUnitIso_inv_naturality_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionHomRight`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionUnitIso_hom_naturality`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionRight_mop`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_def`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_def'`, `CategoryTheory.Functor.OplaxLeftLinear.δₗ_naturality_right_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMop_obj_unmop_map`, `CategoryTheory.Mod_.assoc_flip`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.associator_actionHom`, `CategoryTheory.Functor.LaxLeftLinear.μₗ_associativity_assoc`, `CategoryTheory.ModObj.mul_smul`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction_actionHomRight`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionRight_mop`, `CategoryTheory.ModObj.mul_smul'`, `CategoryTheory.MonoidalCategory.selfLeftAction_actionHomRight`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionUnitIso_inv_naturality`, `CategoryTheory.Functor.OplaxLeftLinear.δₗ_associativity_inv_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedAction_obj_map`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.isIso_actionHomRight`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_def'_assoc`
`actionObj` 📖	CompOp	150 math math: `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionUnitNatIso_inv_app`, `CategoryTheory.ModObj.one_smul_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_hom_inv_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionUnitNatIso_hom_app`, `CategoryTheory.ModObj.mul_smul_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction_actionObj`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_actionHomRight`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_actionAssocIso`, `CategoryTheory.Functor.LaxLeftLinear.μₗ_naturality_right`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_actionHomRight`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.isIso_actionHom`, `CategoryTheory.Functor.LeftLinear.instIsIsoδₗ`, `CategoryTheory.Functor.OplaxLeftLinear.δₗ_associativity_inv`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_actionAssocIso`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftUnitor_actionHom_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.action_exchange`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionAssocNatIso_hom_app_app_app`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_id_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomLeft_action_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_hom_inv`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMopMonoidal_μ_unmop_app`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.isIso_actionHomLeft`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomLeft_action`, `CategoryTheory.ModObj.mul_smul'_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_def_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionUnitIso_hom_naturality_assoc`, `CategoryTheory.Functor.LeftLinear.μₗ_comp_δₗ_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionAssocIso_inv_naturality_assoc`, `CategoryTheory.Functor.LaxLeftLinear.μₗ_associativity_inv_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_comp_assoc`, `CategoryTheory.Functor.LeftLinear.inv_μₗ`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_inv_hom_assoc`, `CategoryTheory.IsMod_Hom.smul_hom`, `CategoryTheory.Functor.LaxLeftLinear.μₗ_naturality_right_assoc`, `CategoryTheory.Functor.OplaxLeftLinear.δₗ_naturality_left_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.id_actionHomLeft`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.inv_actionHomLeft`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.whiskerLeft_actionHomLeft_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.action_exchange_assoc`, `CategoryTheory.Functor.OplaxLeftLinear.δₗ_unitality_hom_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.tensor_actionHomRight`, `CategoryTheory.ModObj.one_smul'_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.rightUnitor_actionHom`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_actionObj`, `CategoryTheory.Functor.OplaxLeftLinear.δₗ_unitality_inv`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_actionHom_unop`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction_actionObj`, `CategoryTheory.Functor.OplaxLeftLinear.δₗ_associativity`, `CategoryTheory.Functor.LeftLinear.δₗ_comp_μₗ`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.hom_inv_actionHomLeft'_assoc`, `CategoryTheory.Functor.LaxLeftLinear.μₗ_unitality_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionAssocNatIso_inv_app_app_app`, `CategoryTheory.IsMod_Hom.smul_hom_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_id`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.id_actionHomLeft_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionAssocIso_hom_naturality`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_actionHomLeft_op`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.unit_actionHomRight_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedAction_map_app`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftUnitor_actionHom`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_inv_hom'_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_actionUnitIso`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_inv_hom'`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.associator_actionHom_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_actionHomLeft_unop`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_actionObj`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionRight_obj`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.hom_inv_actionHomLeft_assoc`, `CategoryTheory.ModObj.one_smul'`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_inv_hom`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.tensor_actionHomRight_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionObj`, `CategoryTheory.Functor.LaxLeftLinear.μₗ_associativity`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_comp_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.rightUnitor_actionHom_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_hom_inv'_assoc`, `CategoryTheory.Functor.OplaxLeftLinear.δₗ_unitality_hom`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_actionAssocIso_unop`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.whiskerLeft_actionHomLeft`, `CategoryTheory.Functor.LaxLeftLinear.μₗ_naturality_left`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionAssocIso_hom_naturality_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_comp`, `CategoryTheory.ModObj.assoc_flip`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_hom_inv'`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMopMonoidal_δ_unmop_app`, `CategoryTheory.MonoidalCategory.selfLeftAction_actionObj`, `CategoryTheory.Functor.OplaxLeftLinear.δₗ_naturality_right`, `CategoryTheory.Functor.OplaxLeftLinear.δₗ_associativity_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_actionRight_op`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.inv_actionHomRight`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionObj_mop`, `CategoryTheory.Functor.LaxLeftLinear.μₗ_associativity_inv`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.unit_actionHomRight`, `CategoryTheory.Functor.LaxLeftLinear.μₗ_unitality_inv`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_actionHom_op`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMop_obj_unmop_obj`, `CategoryTheory.ModObj.one_smul`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_actionRight_unop`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionUnitIso_inv_naturality_assoc`, `CategoryTheory.Functor.LaxLeftLinear.μₗ_unitality`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.whiskerRight_actionHomLeft`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_actionObj_unop`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_actionHom`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionObj`, `CategoryTheory.Functor.LaxLeftLinear.μₗ_unitality_inv_assoc`, `CategoryTheory.Functor.OplaxLeftLinear.δₗ_unitality_inv_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionObj_mop`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.comp_actionHomLeft`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.comp_actionHomLeft_assoc`, `CategoryTheory.Functor.OplaxLeftLinear.δₗ_naturality_left`, `CategoryTheory.Mod_.scalarRestriction_smul`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionAssocIso_inv_naturality`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_actionHom`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.inv_hom_actionHomLeft'_assoc`, `CategoryTheory.Functor.LaxLeftLinear.μₗ_naturality_left_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionUnitIso_hom_naturality`, `CategoryTheory.ModObj.smul_def`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_actionAssocIso_op`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_def`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_def'`, `CategoryTheory.Functor.OplaxLeftLinear.δₗ_naturality_right_assoc`, `CategoryTheory.Functor.LeftLinear.inv_δₗ`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionObj`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.inv_actionHom`, `CategoryTheory.Functor.LeftLinear.μₗ_comp_δₗ`, `CategoryTheory.Mod_.assoc_flip`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_actionHomLeft`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.associator_actionHom`, `CategoryTheory.Functor.LeftLinear.instIsIsoμₗ`, `CategoryTheory.Functor.LaxLeftLinear.μₗ_associativity_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMopMonoidal_η_unmop_app`, `CategoryTheory.ModObj.mul_smul`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMopMonoidal_ε_unmop_app`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.inv_hom_actionHomLeft_assoc`, `CategoryTheory.ModObj.mul_smul'`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionLeft_obj`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.hom_inv_actionHomLeft`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.hom_inv_actionHomLeft'`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_actionObj_op`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionUnitIso_inv_naturality`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_actionUnitIso`, `CategoryTheory.Functor.LeftLinear.δₗ_comp_μₗ_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_actionHomLeft`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_comp`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.inv_hom_actionHomLeft`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedAction_obj_obj`, `CategoryTheory.Functor.OplaxLeftLinear.δₗ_associativity_inv_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.inv_hom_actionHomLeft'`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.isIso_actionHomRight`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_def'_assoc`
`actionUnitIso` 📖	CompOp	36 math math: `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionUnitNatIso_inv_app`, `CategoryTheory.ModObj.one_smul_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionUnitNatIso_hom_app`, `CategoryTheory.MonoidalCategory.selfLeftAction_actionUnitIso`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftUnitor_actionHom_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionUnitIso_hom_naturality_assoc`, `CategoryTheory.Functor.OplaxLeftLinear.δₗ_unitality_hom_assoc`, `CategoryTheory.ModObj.one_smul'_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.rightUnitor_actionHom`, `CategoryTheory.Functor.OplaxLeftLinear.δₗ_unitality_inv`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionUnitIso`, `CategoryTheory.Functor.LaxLeftLinear.μₗ_unitality_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.unit_actionHomRight_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftUnitor_actionHom`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction_actionUnitIso`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction_actionUnitIso`, `CategoryTheory.ModObj.one_smul'`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.rightUnitor_actionHom_assoc`, `CategoryTheory.Functor.OplaxLeftLinear.δₗ_unitality_hom`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction_actionUnitIso`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.unit_actionHomRight`, `CategoryTheory.Functor.LaxLeftLinear.μₗ_unitality_inv`, `CategoryTheory.ModObj.one_smul`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionUnitIso_inv_naturality_assoc`, `CategoryTheory.Functor.LaxLeftLinear.μₗ_unitality`, `CategoryTheory.Functor.LaxLeftLinear.μₗ_unitality_inv_assoc`, `CategoryTheory.Functor.OplaxLeftLinear.δₗ_unitality_inv_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionUnitIso_hom_naturality`, `CategoryTheory.ModObj.smul_def`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionUnitIso_hom`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionUnitIso_inv`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMopMonoidal_η_unmop_app`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMopMonoidal_ε_unmop_app`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionUnitIso_inv_naturality`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_actionUnitIso`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionUnitIso`

CategoryTheory.MonoidalCategory.MonoidalRightAction

Definitions

Name	Category	Theorems
`actionAssocNatIso` 📖	CompOp	2 math math: `actionAssocNatIso_inv_app_app_app`, `actionAssocNatIso_hom_app_app_app`
`actionLeft` 📖	CompOp	2 math math: `actionLeft_obj`, `actionLeft_map`
`actionRight` 📖	CompOp	6 math math: `curriedActionMonoidal_η_app`, `actionRight_obj`, `curriedActionMonoidal_ε_app`, `actionRight_map`, `actionUnitNatIso_hom_app`, `actionUnitNatIso_inv_app`
`actionUnitNatIso` 📖	CompOp	2 math math: `actionUnitNatIso_hom_app`, `actionUnitNatIso_inv_app`
`curriedAction` 📖	CompOp	11 math math: `curriedAction_obj_obj`, `curriedActionActionOfMonoidalFunctorToEndofunctorIso_inv_app_app`, `curriedAction_map_app`, `curriedActionMonoidal_η_app`, `curriedActionActionOfMonoidalFunctorToEndofunctorIso_hom_app_app`, `curriedAction_obj_map`, `actionAssocNatIso_inv_app_app_app`, `curriedActionMonoidal_ε_app`, `curriedActionMonoidal_μ_app`, `curriedActionMonoidal_δ_app`, `actionAssocNatIso_hom_app_app_app`
`termαᵣ` 📖	CompOp	—
`termρᵣ` 📖	CompOp	—
`toMonoidalRightActionStruct` 📖	CompOp	186 math math: `rightActionOfOppositeRightAction_actionRight_unop`, `unit_actionHomRight_assoc`, `actionHomRight_hom_inv'`, `actionHomRight_whiskerRight`, `actionHomRight_comp_assoc`, `CategoryTheory.MonoidalCategory.endofunctorMonoidalCategory.evaluationRightAction_actionHomLeft`, `id_actionHom`, `curriedAction_obj_obj`, `CategoryTheory.Functor.OplaxRightLinear.δᵣ_unitality_inv`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction_actionObj`, `actionAssocIso_inv_naturality`, `CategoryTheory.Functor.OplaxRightLinear.δᵣ_naturality_right_assoc`, `CategoryTheory.Functor.LaxRightLinear.μᵣ_naturality_right_assoc`, `oppositeRightAction_actionObj`, `monoidalOppositeRightAction_actionHomLeft`, `actionHom_associator`, `CategoryTheory.Functor.LaxRightLinear.μᵣ_unitality_inv_assoc`, `oppositeRightAction_actionHomRight`, `actionHom_id`, `actionHom_leftUnitor`, `actionHomRight_hom_inv`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction_actionHom`, `actionHomRight_comp`, `CategoryTheory.MonoidalCategory.endofunctorMonoidalCategory.evaluationRightAction_actionUnitIso`, `CategoryTheory.Functor.LaxRightLinear.μᵣ_associativity_inv_assoc`, `hom_inv_actionHomLeft'_assoc`, `hom_inv_actionHomLeft_assoc`, `actionHom_def'_assoc`, `inv_hom_actionHomLeft`, `isIso_actionHom`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionHomLeft`, `CategoryTheory.Functor.OplaxRightLinear.δᵣ_associativity_inv`, `actionHom_def`, `curriedAction_map_app`, `actionOfMonoidalFunctorToEndofunctor_actionUnitIso_inv`, `actionUnitIso_hom_naturality_assoc`, `curriedActionMonoidal_η_app`, `CategoryTheory.Functor.OplaxRightLinear.δᵣ_unitality_hom_assoc`, `actionHomRight_inv_hom`, `actionOfMonoidalFunctorToEndofunctor_actionUnitIso_hom`, `rightActionOfMonoidalOppositeLeftAction_actionHom`, `monoidalOppositeRightAction_actionAssocIso_mop_mop`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionHomRight`, `actionOfMonoidalFunctorToEndofunctor_actionAssocIso_inv`, `actionHom_comp`, `monoidalOppositeRightAction_actionHom`, `actionHom_def'`, `actionAssocIso_hom_naturality_assoc`, `CategoryTheory.MonoidalCategory.selRightfAction_actionHomRight`, `actionHomLeft_tensor`, `actionAssocIso_hom_naturality`, `actionRight_obj`, `inv_actionHomLeft`, `CategoryTheory.MonoidalCategory.selRightfAction_actionHom`, `CategoryTheory.Functor.OplaxRightLinear.δᵣ_naturality_left`, `CategoryTheory.Functor.RightLinear.μᵣ_comp_δᵣ`, `actionHom_associator_assoc`, `hom_inv_actionHomLeft'`, `id_actionHomLeft_assoc`, `CategoryTheory.MonoidalCategory.endofunctorMonoidalCategory.evaluationRightAction_actionHomRight`, `inv_actionHomRight`, `actionHomRight_whiskerRight_assoc`, `rightActionOfOppositeRightAction_actionHom`, `monoidalOppositeRightAction_actionHomRight_mop`, `monoidalOppositeRightAction_actionAssocIso`, `CategoryTheory.Functor.LaxRightLinear.μᵣ_associativity_inv`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionHomLeft_mop`, `inv_actionHom`, `rightActionOfMonoidalOppositeLeftAction_actionObj`, `actionHomRight_hom_inv'_assoc`, `rightActionOfOppositeRightAction_actionObj`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionUnitIso`, `CategoryTheory.Functor.OplaxRightLinear.δᵣ_associativity`, `CategoryTheory.Functor.RightLinear.δᵣ_comp_μᵣ`, `curriedAction_obj_map`, `action_exchange_assoc`, `rightActionOfOppositeRightAction_actionUnitIso`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionHom_mop_mop`, `actionHom_rightUnitor`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction_actionAssocIso`, `actionHom_def_assoc`, `monoidalOppositeRightAction_actionHomRight`, `rightActionOfOppositeRightAction_actionAssocIso_unop`, `CategoryTheory.Functor.RightLinear.inv_μᵣ`, `rightActionOfOppositeRightAction_actionObj_unop`, `actionHomRight_id_assoc`, `action_actionHomRight_assoc`, `actionAssocNatIso_inv_app_app_app`, `CategoryTheory.MonoidalCategory.selRightfAction_actionUnitIso`, `oppositeRightAction_actionAssocIso_op`, `actionHom_rightUnitor_assoc`, `CategoryTheory.MonoidalCategory.selRightfAction_actionHomLeft`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction_actionUnitIso`, `CategoryTheory.Functor.LaxRightLinear.μᵣ_naturality_right`, `action_exchange`, `CategoryTheory.Functor.RightLinear.instIsIsoμᵣ`, `curriedActionMonoidal_ε_app`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionAssocIso`, `CategoryTheory.Functor.OplaxRightLinear.δᵣ_unitality_hom`, `rightActionOfMonoidalOppositeLeftAction_actionHomLeft`, `CategoryTheory.Functor.RightLinear.instIsIsoδᵣ`, `inv_hom_actionHomLeft_assoc`, `CategoryTheory.Functor.LaxRightLinear.μᵣ_associativity_assoc`, `actionAssocIso_inv_naturality_assoc`, `oppositeRightAction_actionRight_op`, `actionUnitIso_inv_naturality_assoc`, `CategoryTheory.MonoidalCategory.selRightfAction_actionAssocIso_hom`, `id_actionHomLeft`, `rightActionOfOppositeRightAction_actionHom_unop`, `actionUnitIso_inv_naturality`, `actionHom_leftUnitor_assoc`, `rightActionOfMonoidalOppositeLeftAction_actionUnitIso`, `actionHomRight_inv_hom'`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction_actionHomLeft`, `CategoryTheory.MonoidalCategory.selRightfAction_actionAssocIso_inv`, `CategoryTheory.Functor.LaxRightLinear.μᵣ_unitality`, `inv_hom_actionHomLeft'_assoc`, `curriedActionMonoidal_μ_app`, `actionRight_map`, `CategoryTheory.Functor.OplaxRightLinear.δᵣ_associativity_inv_assoc`, `isIso_actionHomLeft`, `actionUnitIso_hom_naturality`, `unit_actionHomRight`, `CategoryTheory.MonoidalCategory.endofunctorMonoidalCategory.evaluationRightAction_actionObj`, `actionHom_comp_assoc`, `monoidalOppositeRightAction_actionObj_mop`, `actionHomLeft_tensor_assoc`, `CategoryTheory.Functor.LaxRightLinear.μᵣ_naturality_left_assoc`, `comp_actionHomLeft_assoc`, `actionHomRight_hom_inv_assoc`, `CategoryTheory.Functor.LaxRightLinear.μᵣ_associativity`, `rightActionOfOppositeRightAction_actionAssocIso`, `rightActionOfOppositeRightAction_actionHomRight`, `actionHomRight_inv_hom'_assoc`, `rightActionOfOppositeRightAction_actionHomLeft`, `CategoryTheory.Functor.OplaxRightLinear.δᵣ_naturality_left_assoc`, `inv_hom_actionHomLeft'`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionObj`, `actionUnitNatIso_hom_app`, `actionHomRight_id`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionObj_mop`, `monoidalOppositeRightAction_actionHom_mop_mop`, `oppositeRightAction_actionHomLeft`, `hom_inv_actionHomLeft`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionHom`, `actionLeft_obj`, `curriedActionMonoidal_δ_app`, `CategoryTheory.MonoidalCategory.endofunctorMonoidalCategory.evaluationRightAction_actionAssocIso`, `actionLeft_map`, `CategoryTheory.Functor.OplaxRightLinear.δᵣ_associativity_assoc`, `CategoryTheory.Functor.LaxRightLinear.μᵣ_unitality_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionRight_mop`, `rightActionOfMonoidalOppositeLeftAction_actionHomRight`, `whiskerRight_actionHomLeft`, `CategoryTheory.Functor.OplaxRightLinear.δᵣ_unitality_inv_assoc`, `CategoryTheory.MonoidalCategory.selRightfAction_actionObj`, `comp_actionHomLeft`, `oppositeRightAction_actionHom_op`, `monoidalOppositeRightAction_actionObj`, `rightActionOfMonoidalOppositeLeftAction_actionAssocIso`, `oppositeRightAction_actionHom`, `actionUnitNatIso_inv_app`, `actionHomRight_inv_hom_assoc`, `oppositeRightAction_actionHomLeft_op`, `CategoryTheory.Functor.LaxRightLinear.μᵣ_naturality_left`, `oppositeRightAction_actionAssocIso`, `actionOfMonoidalFunctorToEndofunctor_actionObj`, `actionAssocNatIso_hom_app_app_app`, `actionOfMonoidalFunctorToEndofunctor_actionHomRight`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction_actionHomRight`, `action_actionHomRight`, `monoidalOppositeRightAction_actionRight_mop`, `CategoryTheory.Functor.RightLinear.δᵣ_comp_μᵣ_assoc`, `actionOfMonoidalFunctorToEndofunctor_actionAssocIso_hom`, `oppositeRightAction_actionObj_op`, `CategoryTheory.Functor.OplaxRightLinear.δᵣ_naturality_right`, `actionOfMonoidalFunctorToEndofunctor_actionHomLeft`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionAssocIso_mop_mop`, `CategoryTheory.Functor.RightLinear.inv_δᵣ`, `isIso_actionHomRight`, `CategoryTheory.Functor.LaxRightLinear.μᵣ_unitality_inv`, `CategoryTheory.Functor.RightLinear.μᵣ_comp_δᵣ_assoc`, `rightActionOfOppositeRightAction_actionHomLeft_unop`, `actionOfMonoidalFunctorToEndofunctor_actionHom`, `oppositeRightAction_actionUnitIso`, `monoidalOppositeRightAction_actionUnitIso`
`«term_⊙ᵣ_»` 📖	CompOp	—
`«term_⊙ᵣₘ_»` 📖	CompOp	—
`«term_⊴ᵣ_»` 📖	CompOp	—
`«term_⊵ᵣ_»` 📖	CompOp	—
`«termρᵣ[_]»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`actionAssocIso_hom_naturality` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom` `CategoryTheory.MonoidalCategoryStruct.tensorHom` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso`	—	—
`actionAssocIso_hom_naturality_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom` `CategoryTheory.MonoidalCategoryStruct.tensorHom` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `actionAssocIso_hom_naturality`
`actionAssocIso_inv_naturality` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso` `CategoryTheory.MonoidalCategoryStruct.tensorHom`	—	`CategoryTheory.Iso.comp_inv_eq` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.inv_comp_eq` `actionAssocIso_hom_naturality`
`actionAssocIso_inv_naturality_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso` `CategoryTheory.MonoidalCategoryStruct.tensorHom`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `actionAssocIso_inv_naturality`
`actionAssocNatIso_hom_app_app_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.bifunctorComp₁₂` `CategoryTheory.MonoidalCategory.curriedTensor` `curriedAction` `CategoryTheory.Functor.flip` `CategoryTheory.bifunctorComp₂₃` `CategoryTheory.Iso.hom` `actionAssocNatIso` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso`	—	—
`actionAssocNatIso_inv_app_app_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.flip` `CategoryTheory.bifunctorComp₂₃` `curriedAction` `CategoryTheory.bifunctorComp₁₂` `CategoryTheory.MonoidalCategory.curriedTensor` `CategoryTheory.Iso.inv` `actionAssocNatIso` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso`	—	—
`actionHomLeft_tensor` 📖	mathematical	—	`CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso` `CategoryTheory.Iso.inv`	—	`CategoryTheory.Category.assoc` `actionAssocIso_hom_naturality` `actionHom_id` `CategoryTheory.MonoidalCategory.tensorHom_id` `CategoryTheory.MonoidalCategory.id_whiskerRight` `CategoryTheory.Iso.hom_inv_id` `CategoryTheory.Category.comp_id`
`actionHomLeft_tensor_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso` `CategoryTheory.Iso.inv`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `actionHomLeft_tensor`
`actionHomRight_comp` 📖	mathematical	—	`CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj`	—	`CategoryTheory.Category.comp_id`
`actionHomRight_comp_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `actionHomRight_comp`
`actionHomRight_hom_inv` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight` `CategoryTheory.Iso.hom` `CategoryTheory.Iso.inv` `CategoryTheory.CategoryStruct.id`	—	`actionHomRight_comp` `CategoryTheory.Iso.hom_inv_id` `actionHomRight_id`
`actionHomRight_hom_inv'` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight` `CategoryTheory.inv` `CategoryTheory.CategoryStruct.id`	—	`actionHomRight_comp` `CategoryTheory.IsIso.hom_inv_id` `actionHomRight_id`
`actionHomRight_hom_inv'_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight` `CategoryTheory.inv`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Category.id_comp` `Mathlib.Tactic.Reassoc.eq_whisker'` `actionHomRight_hom_inv'`
`actionHomRight_hom_inv_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight` `CategoryTheory.Iso.hom` `CategoryTheory.Iso.inv`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Category.id_comp` `Mathlib.Tactic.Reassoc.eq_whisker'` `actionHomRight_hom_inv`
`actionHomRight_id` 📖	mathematical	—	`CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj`	—	—
`actionHomRight_id_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight` `CategoryTheory.CategoryStruct.id`	—	`CategoryTheory.Category.id_comp` `Mathlib.Tactic.Reassoc.eq_whisker'` `actionHomRight_id`
`actionHomRight_inv_hom` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight` `CategoryTheory.Iso.inv` `CategoryTheory.Iso.hom` `CategoryTheory.CategoryStruct.id`	—	`actionHomRight_comp` `CategoryTheory.Iso.inv_hom_id` `actionHomRight_id`
`actionHomRight_inv_hom'` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight` `CategoryTheory.inv` `CategoryTheory.CategoryStruct.id`	—	`actionHomRight_comp` `CategoryTheory.IsIso.inv_hom_id` `actionHomRight_id`
`actionHomRight_inv_hom'_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight` `CategoryTheory.inv`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Category.id_comp` `Mathlib.Tactic.Reassoc.eq_whisker'` `actionHomRight_inv_hom'`
`actionHomRight_inv_hom_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight` `CategoryTheory.Iso.inv` `CategoryTheory.Iso.hom`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Category.id_comp` `Mathlib.Tactic.Reassoc.eq_whisker'` `actionHomRight_inv_hom`
`actionHomRight_whiskerRight` 📖	mathematical	—	`CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategoryStruct.whiskerRight` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft` `CategoryTheory.Iso.inv`	—	—
`actionHomRight_whiskerRight_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight` `CategoryTheory.MonoidalCategoryStruct.whiskerRight` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft` `CategoryTheory.Iso.inv`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `actionHomRight_whiskerRight`
`actionHom_associator` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.associator` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft`	—	—
`actionHom_associator_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.associator` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `actionHom_associator`
`actionHom_comp` 📖	mathematical	—	`CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj`	—	—
`actionHom_comp_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `actionHom_comp`
`actionHom_def` 📖	mathematical	—	`CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight`	—	—
`actionHom_def'` 📖	mathematical	—	`CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft`	—	`actionHom_def` `action_exchange`
`actionHom_def'_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `actionHom_def'`
`actionHom_def_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `actionHom_def`
`actionHom_id` 📖	mathematical	—	`CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft`	—	`actionHom_def` `actionHomRight_id` `CategoryTheory.Category.comp_id`
`actionHom_leftUnitor` 📖	mathematical	—	`CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.leftUnitor` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso`	—	—
`actionHom_leftUnitor_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.leftUnitor` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `actionHom_leftUnitor`
`actionHom_rightUnitor` 📖	mathematical	—	`CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.rightUnitor` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso`	—	—
`actionHom_rightUnitor_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.rightUnitor` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `actionHom_rightUnitor`
`actionLeft_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `actionLeft` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct`	—	—
`actionLeft_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `actionLeft` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct`	—	—
`actionRight_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `actionRight` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct`	—	—
`actionRight_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `actionRight` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct`	—	—
`actionUnitIso_hom_naturality` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft`	—	—
`actionUnitIso_hom_naturality_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `actionUnitIso_hom_naturality`
`actionUnitIso_inv_naturality` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft`	—	`CategoryTheory.Iso.inv_comp_eq` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.comp_inv_eq` `actionUnitIso_hom_naturality`
`actionUnitIso_inv_naturality_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `actionUnitIso_inv_naturality`
`actionUnitNatIso_hom_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `actionRight` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Functor.id` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `actionUnitNatIso` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso`	—	—
`actionUnitNatIso_inv_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Functor.id` `actionRight` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `actionUnitNatIso` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso`	—	—
`action_actionHomRight` 📖	mathematical	—	`CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft` `CategoryTheory.Iso.hom`	—	`whiskerRight_actionHomLeft` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.inv_hom_id` `CategoryTheory.Category.comp_id` `CategoryTheory.Iso.inv_hom_id_assoc`
`action_actionHomRight_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft` `CategoryTheory.Iso.hom`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `action_actionHomRight`
`action_exchange` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft`	—	`CategoryTheory.Category.id_comp` `CategoryTheory.Category.comp_id`
`action_exchange_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `action_exchange`
`comp_actionHomLeft` 📖	mathematical	—	`CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj`	—	`CategoryTheory.Category.id_comp`
`comp_actionHomLeft_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `comp_actionHomLeft`
`curriedAction_map_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft` `CategoryTheory.Functor.map` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `curriedAction` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight`	—	—
`curriedAction_obj_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `curriedAction` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct`	—	—
`curriedAction_obj_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `curriedAction` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct`	—	—
`hom_inv_actionHomLeft` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft` `CategoryTheory.Iso.hom` `CategoryTheory.Iso.inv` `CategoryTheory.CategoryStruct.id`	—	`comp_actionHomLeft` `CategoryTheory.Iso.hom_inv_id` `id_actionHomLeft`
`hom_inv_actionHomLeft'` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft` `CategoryTheory.inv` `CategoryTheory.CategoryStruct.id`	—	`comp_actionHomLeft` `CategoryTheory.IsIso.hom_inv_id` `id_actionHomLeft`
`hom_inv_actionHomLeft'_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft` `CategoryTheory.inv`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Category.id_comp` `Mathlib.Tactic.Reassoc.eq_whisker'` `hom_inv_actionHomLeft'`
`hom_inv_actionHomLeft_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft` `CategoryTheory.Iso.hom` `CategoryTheory.Iso.inv`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Category.id_comp` `Mathlib.Tactic.Reassoc.eq_whisker'` `hom_inv_actionHomLeft`
`id_actionHom` 📖	mathematical	—	`CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight`	—	`actionHom_def` `id_actionHomLeft` `CategoryTheory.Category.id_comp`
`id_actionHomLeft` 📖	mathematical	—	`CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj`	—	—
`id_actionHomLeft_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft` `CategoryTheory.CategoryStruct.id`	—	`CategoryTheory.Category.id_comp` `Mathlib.Tactic.Reassoc.eq_whisker'` `id_actionHomLeft`
`inv_actionHom` 📖	mathematical	—	`CategoryTheory.inv` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom` `isIso_actionHom`	—	`CategoryTheory.IsIso.inv_eq_of_hom_inv_id` `isIso_actionHom` `CategoryTheory.IsIso.hom_inv_id` `actionHom_id` `id_actionHomLeft`
`inv_actionHomLeft` 📖	mathematical	—	`CategoryTheory.inv` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft` `isIso_actionHomLeft`	—	`CategoryTheory.IsIso.inv_eq_of_hom_inv_id` `isIso_actionHomLeft` `hom_inv_actionHomLeft'`
`inv_actionHomRight` 📖	mathematical	—	`CategoryTheory.inv` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight` `isIso_actionHomRight`	—	`CategoryTheory.IsIso.inv_eq_of_hom_inv_id` `isIso_actionHomRight` `actionHomRight_hom_inv'`
`inv_hom_actionHomLeft` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft` `CategoryTheory.Iso.inv` `CategoryTheory.Iso.hom` `CategoryTheory.CategoryStruct.id`	—	`comp_actionHomLeft` `CategoryTheory.Iso.inv_hom_id` `id_actionHomLeft`
`inv_hom_actionHomLeft'` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft` `CategoryTheory.inv` `CategoryTheory.CategoryStruct.id`	—	`comp_actionHomLeft` `CategoryTheory.IsIso.inv_hom_id` `id_actionHomLeft`
`inv_hom_actionHomLeft'_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft` `CategoryTheory.inv`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Category.id_comp` `Mathlib.Tactic.Reassoc.eq_whisker'` `inv_hom_actionHomLeft'`
`inv_hom_actionHomLeft_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft` `CategoryTheory.Iso.inv` `CategoryTheory.Iso.hom`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Category.id_comp` `Mathlib.Tactic.Reassoc.eq_whisker'` `inv_hom_actionHomLeft`
`isIso_actionHom` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom`	—	`CategoryTheory.IsIso.hom_inv_id` `actionHom_id` `id_actionHomLeft` `CategoryTheory.IsIso.inv_hom_id`
`isIso_actionHomLeft` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft`	—	`hom_inv_actionHomLeft'` `inv_hom_actionHomLeft'`
`isIso_actionHomRight` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight`	—	`actionHomRight_hom_inv'` `actionHomRight_inv_hom'`
`unit_actionHomRight` 📖	mathematical	—	`CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso` `CategoryTheory.Iso.inv`	—	`CategoryTheory.Category.assoc` `actionUnitIso_hom_naturality` `CategoryTheory.Iso.hom_inv_id` `CategoryTheory.Category.comp_id`
`unit_actionHomRight_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso` `CategoryTheory.Iso.inv`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `unit_actionHomRight`
`whiskerRight_actionHomLeft` 📖	mathematical	—	`CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso` `CategoryTheory.Iso.inv`	—	—

CategoryTheory.MonoidalCategory.MonoidalRightActionStruct

Definitions

Name	Category	Theorems
`actionAssocIso` 📖	CompOp	44 math math: `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_whiskerRight`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionAssocIso_inv_naturality`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_associator`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_leftUnitor`, `CategoryTheory.Functor.LaxRightLinear.μᵣ_associativity_inv_assoc`, `CategoryTheory.Functor.OplaxRightLinear.δᵣ_associativity_inv`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionAssocIso_mop_mop`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionOfMonoidalFunctorToEndofunctor_actionAssocIso_inv`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionAssocIso_hom_naturality_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomLeft_tensor`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionAssocIso_hom_naturality`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_associator_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_whiskerRight_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionAssocIso`, `CategoryTheory.Functor.LaxRightLinear.μᵣ_associativity_inv`, `CategoryTheory.Functor.OplaxRightLinear.δᵣ_associativity`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_rightUnitor`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction_actionAssocIso`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_actionAssocIso_unop`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.action_actionHomRight_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionAssocNatIso_inv_app_app_app`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.oppositeRightAction_actionAssocIso_op`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_rightUnitor_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionAssocIso`, `CategoryTheory.Functor.LaxRightLinear.μᵣ_associativity_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionAssocIso_inv_naturality_assoc`, `CategoryTheory.MonoidalCategory.selRightfAction_actionAssocIso_hom`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_leftUnitor_assoc`, `CategoryTheory.MonoidalCategory.selRightfAction_actionAssocIso_inv`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedActionMonoidal_μ_app`, `CategoryTheory.Functor.OplaxRightLinear.δᵣ_associativity_inv_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomLeft_tensor_assoc`, `CategoryTheory.Functor.LaxRightLinear.μᵣ_associativity`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_actionAssocIso`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedActionMonoidal_δ_app`, `CategoryTheory.MonoidalCategory.endofunctorMonoidalCategory.evaluationRightAction_actionAssocIso`, `CategoryTheory.Functor.OplaxRightLinear.δᵣ_associativity_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.whiskerRight_actionHomLeft`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction_actionAssocIso`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.oppositeRightAction_actionAssocIso`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionAssocNatIso_hom_app_app_app`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.action_actionHomRight`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionOfMonoidalFunctorToEndofunctor_actionAssocIso_hom`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionAssocIso_mop_mop`
`actionHom` 📖	CompOp	26 math math: `CategoryTheory.MonoidalCategory.MonoidalRightAction.id_actionHom`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionAssocIso_inv_naturality`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_id`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction_actionHom`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_def'_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.isIso_actionHom`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_def`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction_actionHom`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_comp`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionHom`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_def'`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionAssocIso_hom_naturality_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionAssocIso_hom_naturality`, `CategoryTheory.MonoidalCategory.selRightfAction_actionHom`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_actionHom`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.inv_actionHom`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionHom_mop_mop`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_def_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionAssocIso_inv_naturality_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_actionHom_unop`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_comp_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionHom_mop_mop`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionHom`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.oppositeRightAction_actionHom_op`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.oppositeRightAction_actionHom`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionOfMonoidalFunctorToEndofunctor_actionHom`
`actionHomLeft` 📖	CompOp	63 math math: `CategoryTheory.MonoidalCategory.MonoidalRightAction.unit_actionHomRight_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_whiskerRight`, `CategoryTheory.MonoidalCategory.endofunctorMonoidalCategory.evaluationRightAction_actionHomLeft`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionHomLeft`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_associator`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_id`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_leftUnitor`, `CategoryTheory.Functor.LaxRightLinear.μᵣ_associativity_inv_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.hom_inv_actionHomLeft'_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.hom_inv_actionHomLeft_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_def'_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.inv_hom_actionHomLeft`, `CategoryTheory.Functor.OplaxRightLinear.δᵣ_associativity_inv`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_def`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedAction_map_app`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionUnitIso_hom_naturality_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionHomRight`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_def'`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomLeft_tensor`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.inv_actionHomLeft`, `CategoryTheory.Functor.OplaxRightLinear.δᵣ_naturality_left`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_associator_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.hom_inv_actionHomLeft'`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.id_actionHomLeft_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_whiskerRight_assoc`, `CategoryTheory.Functor.LaxRightLinear.μᵣ_associativity_inv`, `CategoryTheory.Functor.OplaxRightLinear.δᵣ_associativity`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedAction_obj_map`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.action_exchange_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_def_assoc`, `CategoryTheory.MonoidalCategory.selRightfAction_actionHomLeft`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.action_exchange`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction_actionHomLeft`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.inv_hom_actionHomLeft_assoc`, `CategoryTheory.Functor.LaxRightLinear.μᵣ_associativity_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionUnitIso_inv_naturality_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.id_actionHomLeft`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionUnitIso_inv_naturality`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_leftUnitor_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.inv_hom_actionHomLeft'_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionRight_map`, `CategoryTheory.Functor.OplaxRightLinear.δᵣ_associativity_inv_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.isIso_actionHomLeft`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionUnitIso_hom_naturality`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.unit_actionHomRight`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomLeft_tensor_assoc`, `CategoryTheory.Functor.LaxRightLinear.μᵣ_naturality_left_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.comp_actionHomLeft_assoc`, `CategoryTheory.Functor.LaxRightLinear.μᵣ_associativity`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_actionHomLeft`, `CategoryTheory.Functor.OplaxRightLinear.δᵣ_naturality_left_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.inv_hom_actionHomLeft'`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.oppositeRightAction_actionHomLeft`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.hom_inv_actionHomLeft`, `CategoryTheory.Functor.OplaxRightLinear.δᵣ_associativity_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionRight_mop`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.comp_actionHomLeft`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.oppositeRightAction_actionHomLeft_op`, `CategoryTheory.Functor.LaxRightLinear.μᵣ_naturality_left`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction_actionHomRight`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionRight_mop`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionOfMonoidalFunctorToEndofunctor_actionHomLeft`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_actionHomLeft_unop`
`actionHomRight` 📖	CompOp	51 math math: `CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_actionRight_unop`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_hom_inv'`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_whiskerRight`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_comp_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.id_actionHom`, `CategoryTheory.Functor.OplaxRightLinear.δᵣ_naturality_right_assoc`, `CategoryTheory.Functor.LaxRightLinear.μᵣ_naturality_right_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_associator`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.oppositeRightAction_actionHomRight`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_leftUnitor`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_hom_inv`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_comp`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_def'_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionHomLeft`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_def`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedAction_map_app`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_inv_hom`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_def'`, `CategoryTheory.MonoidalCategory.selRightfAction_actionHomRight`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_associator_assoc`, `CategoryTheory.MonoidalCategory.endofunctorMonoidalCategory.evaluationRightAction_actionHomRight`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.inv_actionHomRight`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_whiskerRight_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionHomRight_mop`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionHomLeft_mop`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_hom_inv'_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.action_exchange_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_rightUnitor`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_def_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionHomRight`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_id_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.action_actionHomRight_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_rightUnitor_assoc`, `CategoryTheory.Functor.LaxRightLinear.μᵣ_naturality_right`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.action_exchange`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.oppositeRightAction_actionRight_op`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_leftUnitor_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_inv_hom'`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction_actionHomLeft`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_hom_inv_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_actionHomRight`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_inv_hom'_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_id`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionLeft_map`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction_actionHomRight`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.whiskerRight_actionHomLeft`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_inv_hom_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionOfMonoidalFunctorToEndofunctor_actionHomRight`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.action_actionHomRight`, `CategoryTheory.Functor.OplaxRightLinear.δᵣ_naturality_right`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.isIso_actionHomRight`
`actionObj` 📖	CompOp	136 math math: `CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_actionRight_unop`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.unit_actionHomRight_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_hom_inv'`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_whiskerRight`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_comp_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedAction_obj_obj`, `CategoryTheory.Functor.OplaxRightLinear.δᵣ_unitality_inv`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction_actionObj`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionAssocIso_inv_naturality`, `CategoryTheory.Functor.OplaxRightLinear.δᵣ_naturality_right_assoc`, `CategoryTheory.Functor.LaxRightLinear.μᵣ_naturality_right_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.oppositeRightAction_actionObj`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_associator`, `CategoryTheory.Functor.LaxRightLinear.μᵣ_unitality_inv_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.oppositeRightAction_actionHomRight`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_leftUnitor`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_hom_inv`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_comp`, `CategoryTheory.Functor.LaxRightLinear.μᵣ_associativity_inv_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.hom_inv_actionHomLeft'_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.hom_inv_actionHomLeft_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_def'_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.inv_hom_actionHomLeft`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.isIso_actionHom`, `CategoryTheory.Functor.OplaxRightLinear.δᵣ_associativity_inv`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_def`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedAction_map_app`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionUnitIso_hom_naturality_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedActionMonoidal_η_app`, `CategoryTheory.Functor.OplaxRightLinear.δᵣ_unitality_hom_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_inv_hom`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_comp`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_def'`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionAssocIso_hom_naturality_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomLeft_tensor`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionAssocIso_hom_naturality`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionRight_obj`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.inv_actionHomLeft`, `CategoryTheory.Functor.OplaxRightLinear.δᵣ_naturality_left`, `CategoryTheory.Functor.RightLinear.μᵣ_comp_δᵣ`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_associator_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.hom_inv_actionHomLeft'`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.id_actionHomLeft_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.inv_actionHomRight`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_whiskerRight_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_actionHom`, `CategoryTheory.Functor.LaxRightLinear.μᵣ_associativity_inv`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.inv_actionHom`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction_actionObj`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_hom_inv'_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_actionObj`, `CategoryTheory.Functor.OplaxRightLinear.δᵣ_associativity`, `CategoryTheory.Functor.RightLinear.δᵣ_comp_μᵣ`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.action_exchange_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_actionUnitIso`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_rightUnitor`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_def_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_actionAssocIso_unop`, `CategoryTheory.Functor.RightLinear.inv_μᵣ`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_actionObj_unop`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_id_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.action_actionHomRight_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionAssocNatIso_inv_app_app_app`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.oppositeRightAction_actionAssocIso_op`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_rightUnitor_assoc`, `CategoryTheory.Functor.LaxRightLinear.μᵣ_naturality_right`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.action_exchange`, `CategoryTheory.Functor.RightLinear.instIsIsoμᵣ`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedActionMonoidal_ε_app`, `CategoryTheory.Functor.OplaxRightLinear.δᵣ_unitality_hom`, `CategoryTheory.Functor.RightLinear.instIsIsoδᵣ`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.inv_hom_actionHomLeft_assoc`, `CategoryTheory.Functor.LaxRightLinear.μᵣ_associativity_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionAssocIso_inv_naturality_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.oppositeRightAction_actionRight_op`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionUnitIso_inv_naturality_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.id_actionHomLeft`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_actionHom_unop`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionUnitIso_inv_naturality`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_leftUnitor_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_inv_hom'`, `CategoryTheory.Functor.LaxRightLinear.μᵣ_unitality`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.inv_hom_actionHomLeft'_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedActionMonoidal_μ_app`, `CategoryTheory.Functor.OplaxRightLinear.δᵣ_associativity_inv_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.isIso_actionHomLeft`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionUnitIso_hom_naturality`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.unit_actionHomRight`, `CategoryTheory.MonoidalCategory.endofunctorMonoidalCategory.evaluationRightAction_actionObj`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_comp_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionObj_mop`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomLeft_tensor_assoc`, `CategoryTheory.Functor.LaxRightLinear.μᵣ_naturality_left_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.comp_actionHomLeft_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_hom_inv_assoc`, `CategoryTheory.Functor.LaxRightLinear.μᵣ_associativity`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_actionAssocIso`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_actionHomRight`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_inv_hom'_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_actionHomLeft`, `CategoryTheory.Functor.OplaxRightLinear.δᵣ_naturality_left_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.inv_hom_actionHomLeft'`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionObj`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionUnitNatIso_hom_app`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_id`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionObj_mop`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.oppositeRightAction_actionHomLeft`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.hom_inv_actionHomLeft`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionLeft_obj`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedActionMonoidal_δ_app`, `CategoryTheory.Functor.OplaxRightLinear.δᵣ_associativity_assoc`, `CategoryTheory.Functor.LaxRightLinear.μᵣ_unitality_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.whiskerRight_actionHomLeft`, `CategoryTheory.Functor.OplaxRightLinear.δᵣ_unitality_inv_assoc`, `CategoryTheory.MonoidalCategory.selRightfAction_actionObj`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.comp_actionHomLeft`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.oppositeRightAction_actionHom_op`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionObj`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.oppositeRightAction_actionHom`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionUnitNatIso_inv_app`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_inv_hom_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.oppositeRightAction_actionHomLeft_op`, `CategoryTheory.Functor.LaxRightLinear.μᵣ_naturality_left`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.oppositeRightAction_actionAssocIso`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionOfMonoidalFunctorToEndofunctor_actionObj`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionAssocNatIso_hom_app_app_app`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.action_actionHomRight`, `CategoryTheory.Functor.RightLinear.δᵣ_comp_μᵣ_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.oppositeRightAction_actionObj_op`, `CategoryTheory.Functor.OplaxRightLinear.δᵣ_naturality_right`, `CategoryTheory.Functor.RightLinear.inv_δᵣ`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.isIso_actionHomRight`, `CategoryTheory.Functor.LaxRightLinear.μᵣ_unitality_inv`, `CategoryTheory.Functor.RightLinear.μᵣ_comp_δᵣ_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_actionHomLeft_unop`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.oppositeRightAction_actionUnitIso`
`actionUnitIso` 📖	CompOp	32 math math: `CategoryTheory.MonoidalCategory.MonoidalRightAction.unit_actionHomRight_assoc`, `CategoryTheory.Functor.OplaxRightLinear.δᵣ_unitality_inv`, `CategoryTheory.Functor.LaxRightLinear.μᵣ_unitality_inv_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_leftUnitor`, `CategoryTheory.MonoidalCategory.endofunctorMonoidalCategory.evaluationRightAction_actionUnitIso`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionOfMonoidalFunctorToEndofunctor_actionUnitIso_inv`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionUnitIso_hom_naturality_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedActionMonoidal_η_app`, `CategoryTheory.Functor.OplaxRightLinear.δᵣ_unitality_hom_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionOfMonoidalFunctorToEndofunctor_actionUnitIso_hom`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionUnitIso`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_actionUnitIso`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_rightUnitor`, `CategoryTheory.MonoidalCategory.selRightfAction_actionUnitIso`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_rightUnitor_assoc`, `CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfMonoidalOppositeRightAction_actionUnitIso`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedActionMonoidal_ε_app`, `CategoryTheory.Functor.OplaxRightLinear.δᵣ_unitality_hom`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionUnitIso_inv_naturality_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionUnitIso_inv_naturality`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_leftUnitor_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfMonoidalOppositeLeftAction_actionUnitIso`, `CategoryTheory.Functor.LaxRightLinear.μᵣ_unitality`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionUnitIso_hom_naturality`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.unit_actionHomRight`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionUnitNatIso_hom_app`, `CategoryTheory.Functor.LaxRightLinear.μᵣ_unitality_assoc`, `CategoryTheory.Functor.OplaxRightLinear.δᵣ_unitality_inv_assoc`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.actionUnitNatIso_inv_app`, `CategoryTheory.Functor.LaxRightLinear.μᵣ_unitality_inv`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.oppositeRightAction_actionUnitIso`, `CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionUnitIso`

---

← Back to Index