Theorem PrimeSpectrum.punit

Modification history

2023-10-03 07:51
Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean
feat: some golfing in AlgebraicGeometry.PrimeSpectrum.Basic (#7373)
Deleted PrimeSpectrum.punitView on Github →
2023-08-28 19:47
Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean
chore: tidy various files (#6577)
Added PrimeSpectrum.punitView on Github →