feat(RingTheory): Surjective on stalks ring homomorphisms.

[erdOne]

---

[github-actions[bot]]

PR summary 078b7b8ef6

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.RingTheory.SurjectiveOnStalks	1185
Mathlib.AlgebraicGeometry.PrimeSpectrum.TensorProduct	1292

---

Declarations diff

+ IsBasis.le_iff + PrimeSpectrum.continuous_tensorProductTo + PrimeSpectrum.embedding_tensorProductTo_of_surjectiveOnStalks + PrimeSpectrum.embedding_tensorProductTo_of_surjectiveOnStalks_aux + PrimeSpectrum.tensorProductTo + SurjectiveOnStalks + SurjectiveOnStalks.baseChange + SurjectiveOnStalks.comp + SurjectiveOnStalks.exists_mul_eq_tmul + SurjectiveOnStalks.of_comp + surjectiveOnStalks_iff_forall_ideal + surjectiveOnStalks_iff_forall_maximal + surjectiveOnStalks_iff_forall_maximal' + surjectiveOnStalks_iff_of_isLocalRingHom + surjectiveOnStalks_of_exists_div + surjectiveOnStalks_of_isLocalization + surjectiveOnStalks_of_surjective + surjective_localRingHom_iff

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

[mathlib-bors[bot]]

:v: erdOne can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[erdOne]

Thanks for the reviews! bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style