Theorem CategoryTheory.Grothendieck.fiber_eqToHom

Modification history

2025-02-02 17:46
Mathlib/CategoryTheory/Grothendieck.lean
feat(CategoryTheory/Grothendieck): transport; pre preserves equivalences of categories (#19484) …
Added CategoryTheory.Grothendieck.fiber_eqToHomView on Github →