Theorem AlgebraicGeometry.HasRingHomProperty.iff_exists_appLE_locally

Modification history

2024-11-11 10:49
Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean
refactor(AlgebraicGeometry): weaken `RingHom.PropertyIsLocal` (#18717)
Modified AlgebraicGeometry.HasRingHomProperty.iff_exists_appLE_locallyView on Github →
2024-10-16 05:50
Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean
feat(AlgebraicGeometry/RingHomProperties): a property induced from `Locally Q` is equivalent to locally `Q` (#17305) …
Added AlgebraicGeometry.HasRingHomProperty.iff_exists_appLE_locallyView on Github →