Theorem AlgebraicGeometry.HasRingHomProperty.iff_exists_appLE

Modification history

2024-11-11 10:49

Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean

refactor(AlgebraicGeometry): weaken `RingHom.PropertyIsLocal` (#18717)

Modified AlgebraicGeometry.HasRingHomProperty.iff_exists_appLE View on Github →

2024-10-15 08:58

Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean

feat(AlgebraicGeometry): api for morphism properties local at the source and target (#17302) …

Added AlgebraicGeometry.HasRingHomProperty.iff_exists_appLE View on Github →