Theorem PrimeSpectrum.exists_image_comap_of_finite_of_free

Modification history

2024-12-23 15:20
Mathlib/AlgebraicGeometry/PrimeSpectrum/Polynomial.lean
feat(AlgebraicGeometry): `Spec R[X] -> Spec R` is open (#20159)
Added PrimeSpectrum.exists_image_comap_of_finite_of_freeView on Github →