Section7
📁 Source: Hochster/Section7.lean
Statistics
| Metric | Count |
|---|---|
| 4 | |
Theoremsexists_nonempty_homeomorph | 1 |
| Total | 5 |
SpectralSpace
Definitions
| Name | Category | Theorems |
|---|---|---|
firstSWI 📖 | CompOp | — |
hochsterRing 📖 | CompOp | — |
homeomorph 📖 | CompOp | — |
instCommRingHochsterRing 📖 | CompOp | — |
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
exists_nonempty_homeomorph 📖 | — | — | — | — | — |
---