theorem TensorCategories.evaluation_ne_zero_of_nonzero_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.RightRigidCategory C] [CategoryTheory.MonoidalPreadditive C] (X : C) (hX : ¬CategoryTheory.Limits.IsZero X) : ε_ X Xᘁ ≠ 0

The evaluation morphism ε_ X Xᘁ : X ⊗ X* → 𝟙 is nonzero whenever X is nonzero, in a preadditive right-rigid monoidal category.