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