Theorem AlgebraicGeometry.FormallyUnramified.AlgebraicGeometry.FormallyUnramified.isOpenImmersion_diagonal

Modification history

2025-05-04 20:18
Mathlib/AlgebraicGeometry/Morphisms/FormallyUnramified.lean
feat(AlgebraicGeometry): the small étale site (#24568) …
Deleted AlgebraicGeometry.FormallyUnramified.AlgebraicGeometry.FormallyUnramified.isOpenImmersion_diagonalView on Github →
2025-02-04 09:16
Mathlib/AlgebraicGeometry/Morphisms/FormallyUnramified.lean
feat(AlgebraicGeometry): the diagonal of an unramified morphism is an open immersion (#21386)
Added AlgebraicGeometry.FormallyUnramified.AlgebraicGeometry.FormallyUnramified.isOpenImmersion_diagonalView on Github →