Theorem AlgebraicGeometry.HasRingHomProperty.isMultiplicative

Modification history

2024-09-19 10:59
Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean
chore(AlgebraicGeometry): weaken assumptions on local ring hom properties (#16897) …
Added AlgebraicGeometry.HasRingHomProperty.isMultiplicativeView on Github →