Theorem AlgebraicGeometry.isOpenImmersion_sigmaDesc

Modification history

2025-03-10 20:54
Mathlib/AlgebraicGeometry/Limits.lean
feat(AlgebraicGeometry): constructor for `IsColimit (Cofan.mk S f)` (#22541) …
Modified AlgebraicGeometry.isOpenImmersion_sigmaDescView on Github →
2025-01-30 15:54
Mathlib/AlgebraicGeometry/Limits.lean
feat(AlgebraicGeometry): `Π Rᵢ`-points of schemes (#20494)
Added AlgebraicGeometry.isOpenImmersion_sigmaDescView on Github →