2026-01-30 07:22
Mathlib/CategoryTheory/Sites/Subcanonical.lean
feat(CategoryTheory): the yoneda embedding to sheaves preserves disjoint coproducts (#34145) …
Added CategoryTheory.GrothendieckTopology.preservesColimitsOfShape_yoneda_of_ofArrows_inj_mem