class TensorNondegenerate (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] : Prop

Nondegeneracy of the tensor product in an abelian monoidal category: tensoring with self detects zero, and the right dual is zero iff the object is zero.

• isZero_of_tensor_self_isZero (X : C) : CategoryTheory.Limits.IsZero (CategoryTheory.MonoidalCategoryStruct.tensorObj X X) → CategoryTheory.Limits.IsZero X
• isZero_rightDual_of_isZero (X : C) [CategoryTheory.HasRightDual X] : CategoryTheory.Limits.IsZero X → CategoryTheory.Limits.IsZero Xᘁ
• isZero_of_isZero_rightDual (X : C) [CategoryTheory.HasRightDual X] : CategoryTheory.Limits.IsZero Xᘁ → CategoryTheory.Limits.IsZero X

instance tensorNondegenerate_of_rigidCategory (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.RigidCategory C] [CategoryTheory.BraidedCategory C] : TensorNondegenerate C

Any rigid braided abelian monoidal preadditive category has a nondegenerate tensor product.