Theorem CategoryTheory.Equivalence.unitInv_app_inverse

Modification history

2026-03-16 18:02
Mathlib/CategoryTheory/Equivalence.lean
feat(CategoryTheory/Equivalence): tag `Equivalence` with `to_dual` (#36579) …
Deleted CategoryTheory.Equivalence.unitInv_app_inverseView on Github →
2023-02-11 09:23
Mathlib/CategoryTheory/Equivalence.lean
feat: port CategoryTheory.Equivalence (#1287) …
Added CategoryTheory.Equivalence.unitInv_app_inverseView on Github →