Theorem CategoryTheory.PreZeroHypercover.shrink_eq_shrink_of_presieve₀_eq_presieve₀

Modification history

2025-10-25 22:49
Mathlib/CategoryTheory/Sites/Hypercover/Zero.lean
feat(CategoryTheory/Sites): more API for zero hypercovers (#30906) …
Added CategoryTheory.PreZeroHypercover.shrink_eq_shrink_of_presieve₀_eq_presieve₀View on Github →