Def CategoryTheory.Grothendieck.transport

Modification history

2025-02-02 17:46

Mathlib/CategoryTheory/Grothendieck.lean

feat(CategoryTheory/Grothendieck): transport; pre preserves equivalences of categories (#19484) …

Added CategoryTheory.Grothendieck.transport View on Github →