Theorem AlgebraicGeometry.HasRingHomProperty.of_isOpenImmersion

Modification history

2024-09-19 10:59

Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean

chore(AlgebraicGeometry): weaken assumptions on local ring hom properties (#16897) …

Modified AlgebraicGeometry.HasRingHomProperty.of_isOpenImmersion View on Github →

2024-07-23 19:33

Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean

refactor(AlgebraicGeometry): Introduce `HasRingHomProperty`. (#14992) …

Added AlgebraicGeometry.HasRingHomProperty.of_isOpenImmersion View on Github →