Theorem AlgebraicGeometry.isIso_of_isOpenImmersion_of_opensRange_eq_top

Modification history

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