@[reducible, inline]

abbrev TensorCategories.IsLocallyFinite (k : Type u_1) [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Abelian C] : Prop

Abbreviation for LocallyFiniteCategory: a k-linear abelian category is locally finite if it is essentially small, all Hom spaces are finite dimensional, and every object has finite length.

@[reducible, inline]

abbrev TensorCategories.Definition_1_12_1_LocallyFinite (k : Type u_1) [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Abelian C] : Prop

Definition 1.12.1: A k-linear abelian category is locally finite if it is essentially small, all Hom spaces are finite dimensional, and every object has finite length.