Documentation Verification Report

Basic

📁 Source: Mathlib/RingTheory/Spectrum/Maximal/Basic.lean

Statistics

Metric	Count
Definitions `equivSubtype`, `toPrimeSpectrum`	2
Theorems `equivSubtype_apply_coe`, `equivSubtype_symm_apply_asIdeal`, `instNonemptyOfNontrivial`, `range_asIdeal`, `toPrimeSpectrum_injective`	5
Total	7

MaximalSpectrum

Definitions

Name	Category	Theorems
`equivSubtype` 📖	CompOp	2 math math: `equivSubtype_symm_apply_asIdeal`, `equivSubtype_apply_coe`
`toPrimeSpectrum` 📖	CompOp	3 math math: `toPrimeSpectrum_continuous`, `toPrimeSpectrum_injective`, `toPrimeSpectrum_range`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equivSubtype_apply_coe` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `Ideal.IsMaximal` `DFunLike.coe` `Equiv` `MaximalSpectrum` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivSubtype` `asIdeal`	—	—
`equivSubtype_symm_apply_asIdeal` 📖	mathematical	—	`asIdeal` `DFunLike.coe` `Equiv` `Ideal` `CommSemiring.toSemiring` `Ideal.IsMaximal` `MaximalSpectrum` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivSubtype`	—	—
`instNonemptyOfNontrivial` 📖	mathematical	—	`MaximalSpectrum`	—	`Ideal.exists_maximal`
`range_asIdeal` 📖	mathematical	—	`Set.range` `Ideal` `CommSemiring.toSemiring` `MaximalSpectrum` `asIdeal` `setOf` `Ideal.IsMaximal`	—	`Set.ext` `Set.mem_range` `Set.mem_setOf` `isMaximal`
`toPrimeSpectrum_injective` 📖	mathematical	—	`MaximalSpectrum` `PrimeSpectrum` `toPrimeSpectrum`	—	`PrimeSpectrum.ext_iff`

---

← Back to Index