Theorem CategoryTheory.Grothendieck.pre_comp_map_assoc

Modification history

2025-12-13 14:21
Mathlib/CategoryTheory/Grothendieck.lean
chore: use `Category*` everywhere (#32842) …
Modified CategoryTheory.Grothendieck.pre_comp_map_assocView on Github →
2025-07-04 07:44
Mathlib/CategoryTheory/Grothendieck.lean
chore: further whitespace fixes (#26708) …
Modified CategoryTheory.Grothendieck.pre_comp_map_assocView on Github →
2025-02-02 17:46
Mathlib/CategoryTheory/Grothendieck.lean
feat(CategoryTheory/Grothendieck): transport; pre preserves equivalences of categories (#19484) …
Added CategoryTheory.Grothendieck.pre_comp_map_assocView on Github →