Commit 2023-06-05 01:30 8951bb64

View on Github →

feat: port CategoryTheory.Monoidal.Rigid.OfEquivalence (#4660)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Monoidal/Rigid/OfEquivalence.lean

added def CategoryTheory.exactPairingOfFaithful

added def CategoryTheory.exactPairingOfFullyFaithful

added def CategoryTheory.hasLeftDualOfEquivalence

added def CategoryTheory.hasRightDualOfEquivalence

added def CategoryTheory.leftRigidCategoryOfEquivalence

added def CategoryTheory.rightRigidCategoryOfEquivalence

added def CategoryTheory.rigidCategoryOfEquivalence