Theorem PrimeSpectrum.exists_idempotent_basicOpen_eq_of_is_clopen

Modification history