Theorem AlgebraicGeometry.HasRingHomProperty.copy

Modification history

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.copyView on Github →