Theorem AlgebraicGeometry.Ideal.span_eq_top_of_span_image_evalRingHom

Modification history

2025-01-30 15:54
Mathlib/AlgebraicGeometry/PointsPi.lean
feat(AlgebraicGeometry): `Π Rᵢ`-points of schemes (#20494)
Added AlgebraicGeometry.Ideal.span_eq_top_of_span_image_evalRingHomView on Github →