Theorem AlgebraicGeometry.HasRingHomProperty.containsIdentities

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