Theorem AlgebraicGeometry.nonempty_isColimit_binaryCofanMk_of_isCompl

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_binaryCofanMk_of_isComplView on Github →