def CategoryTheory.IsZeroCategory (M : Type u_1) [Category.{u_2, u_1} M] : Prop

A category is a zero category if every one of its objects is a zero object.

class CategoryTheory.IsIndecomposableModuleCategory (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (M : Type u₂) [Category.{v₂, u₂} M] [LeftModuleCategory C M] : Prop

A module category M over a monoidal category C is indecomposable if whenever it is equivalent (as a C-module category) to a direct sum M₁ × M₂, one of the summands is empty.

• indecomp (M₁ M₂ : Type u₂) [Category.{v₂, u₂} M₁] [Category.{v₂, u₂} M₂] [LeftModuleCategory C M₁] [LeftModuleCategory C M₂] : ∀ (x : ModuleEquivalence C M (M₁ × M₂)), IsEmpty M₁ ∨ IsEmpty M₂

@[reducible, inline]

abbrev CategoryTheory.Definition_2_4_3 (C : Type u_1) [Category.{u_2, u_1} C] [MonoidalCategory C] (M : Type u_3) [Category.{u_4, u_3} M] [LeftModuleCategory C M] : Prop

Definition 2.4.3: a module category M over C is indecomposable if it is not equivalent to a nontrivial direct sum of module categories (with both summands nonzero).