Theorem CategoryTheory.MorphismProperty.Under.forget_comp_forget_map

Modification history

2025-12-03 12:21
Mathlib/CategoryTheory/MorphismProperty/Comma.lean
feat(AlgebraicGeometry): locally directed colimits in `P.Over ⊤ S` (#30140) …
Added CategoryTheory.MorphismProperty.Under.forget_comp_forget_mapView on Github →