Theorem CategoryTheory.MorphismProperty.Over.changeProp_obj_left

Modification history

2026-03-04 16:50
Mathlib/CategoryTheory/MorphismProperty/Comma.lean
feat(CategoryTheory/MorphismProperty): API for sites on `P.Over ⊤ X` (#36126) …
Added CategoryTheory.MorphismProperty.Over.changeProp_obj_leftView on Github →