Theorem CategoryTheory.MorphismProperty.IsLocalAtSource.iff_of_zeroHypercover

Modification history

2025-10-03 22:56
Mathlib/CategoryTheory/MorphismProperty/Local.lean
feat(CategoryTheory/MorphismProperty): locality conditions (#30164) …
Added CategoryTheory.MorphismProperty.IsLocalAtSource.iff_of_zeroHypercoverView on Github →