Theorem RingHom.PropertyIsLocal.hasAffinePropertyAffineLocally

Modification history

2024-07-23 19:33

Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean

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

Deleted RingHom.PropertyIsLocal.hasAffinePropertyAffineLocally View on Github →

2024-07-18 12:08

Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean

refactor(AlgebraicGeometry): Rework `Morphisms/Basic` to phase away from TFAEs (#14430) …

Added RingHom.PropertyIsLocal.hasAffinePropertyAffineLocally View on Github →