Def PrimeSpectrum.tensorProductTo

Modification history

2024-07-26 10:22

Mathlib/AlgebraicGeometry/PrimeSpectrum/TensorProduct.lean

feat(RingTheory): Surjective on stalks ring homomorphisms. (#14377)

Added PrimeSpectrum.tensorProductTo View on Github →