Theorem AlgebraicGeometry.nonempty_isColimit_cofanMk_of

Modification history

2025-03-10 20:54
Mathlib/AlgebraicGeometry/Limits.lean
feat(AlgebraicGeometry): constructor for `IsColimit (Cofan.mk S f)` (#22541) …
Added AlgebraicGeometry.nonempty_isColimit_cofanMk_ofView on Github →