Theorem AlgebraicGeometry.SurjectiveOnStalks.mono_of_injective

Modification history

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