2026-05-29 00:22
Mathlib/CategoryTheory/MorphismProperty/Local.lean
refactor(CategoryTheory): redefine `MorphismProperty.IsLocalAtTarget` in terms of presieves (#39978) …
Added CategoryTheory.MorphismProperty.IsLocalAtSource.mk_of_iff_of_zeroHypercover