Theorem PrimeSpectrum.specComap_surjective_of_faithfullyFlat

Modification history

2025-02-12 21:23
Mathlib/RingTheory/Flat/FaithfullyFlat/Algebra.lean
feat(RingTheory/FaithfullyFlat): equivalent characterizations for algebras (#20725) …
Added PrimeSpectrum.specComap_surjective_of_faithfullyFlatView on Github →