Theorem CategoryTheory.Equivalence.counitInv_naturality

Modification history

2026-03-16 18:02

Mathlib/CategoryTheory/Equivalence.lean

feat(CategoryTheory/Equivalence): tag `Equivalence` with `to_dual` (#36579) …

Deleted CategoryTheory.Equivalence.counitInv_naturality View on Github →

2025-04-09 15:42

Mathlib/CategoryTheory/Equivalence.lean

chore(CategoryTheory/Equivalence): simp lemmas for co/unit naturality (#23724) …

Added CategoryTheory.Equivalence.counitInv_naturality View on Github →