Theorem PrimeSpectrum.comapEquiv_symm

Modification history

2026-01-06 11:03
Mathlib/RingTheory/Spectrum/Prime/RingHom.lean
feat(RingTheory): construct etale neighborhood that isolates point in fiber (#32823)
Added PrimeSpectrum.comapEquiv_symmView on Github →