Documentation Verification Report

Defs

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

Statistics

Metric	Count
Definitions `MaximalSpectrum`, `asIdeal`	2
Theorems `ext`, `ext_iff`, `isMaximal`	3
Total	5

MaximalSpectrum

Definitions

Name	Category	Theorems
`asIdeal` 📖	CompOp	22 math math: `mapPiLocalization_bijective`, `IsArtinianRing.primeSpectrum_asIdeal_range_eq`, `toPiLocalization_apply_apply`, `mapPiLocalization_naturality`, `isMaximal`, `range_asIdeal`, `mapPiLocalization_id`, `equivSubtype_symm_apply_asIdeal`, `IsArtinianRing.primeSpectrumEquivMaximalSpectrum_apply_asIdeal`, `IsArtinianRing.primeSpectrumEquivMaximalSpectrum_symm_apply_asIdeal`, `equivSubtype_apply_coe`, `PrimeSpectrum.piLocalizationToMaximal_comp_toPiLocalization`, `PrimeSpectrum.piLocalizationToMaximal_surjective`, `mapPiLocalization_comp`, `iInf_localization_eq_bot`, `toPiLocalization_injective`, `IsArtinianRing.primeSpectrumEquivMaximalSpectrum_comp_asIdeal`, `toPiLocalization_not_surjective_of_infinite`, `PrimeSpectrum.piLocalizationToMaximal_bijective`, `IsArtinianRing.primeSpectrumEquivMaximalSpectrum_symm_comp_asIdeal`, `ext_iff`, `PrimeSpectrum.maximalSpectrumToPiLocalization_surjective_of_discreteTopology`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`asIdeal`	—	—	—
`ext_iff` 📖	mathematical	—	`asIdeal`	—	`ext`
`isMaximal` 📖	mathematical	—	`Ideal.IsMaximal` `CommSemiring.toSemiring` `asIdeal`	—	—

(root)

Definitions

Name	Category	Theorems
`MaximalSpectrum` 📖	CompData	28 math math: `MaximalSpectrum.mapPiLocalization_bijective`, `IsArtinianRing.primeSpectrum_asIdeal_range_eq`, `MaximalSpectrum.toPiLocalization_apply_apply`, `MaximalSpectrum.instT1Space`, `MaximalSpectrum.mapPiLocalization_naturality`, `MaximalSpectrum.toPrimeSpectrum_continuous`, `MaximalSpectrum.range_asIdeal`, `MaximalSpectrum.mapPiLocalization_id`, `MaximalSpectrum.equivSubtype_symm_apply_asIdeal`, `IsArtinianRing.primeSpectrumEquivMaximalSpectrum_apply_asIdeal`, `IsArtinianRing.primeSpectrumEquivMaximalSpectrum_symm_apply_asIdeal`, `MaximalSpectrum.equivSubtype_apply_coe`, `instFiniteMaximalSpectrumOfIsFractionRing`, `PrimeSpectrum.piLocalizationToMaximal_comp_toPiLocalization`, `PrimeSpectrum.piLocalizationToMaximal_surjective`, `IsLocalRing.not_isLocalRing_tfae`, `MaximalSpectrum.toPrimeSpectrum_injective`, `MaximalSpectrum.mapPiLocalization_comp`, `MaximalSpectrum.toPrimeSpectrum_range`, `MaximalSpectrum.iInf_localization_eq_bot`, `MaximalSpectrum.toPiLocalization_injective`, `IsArtinianRing.primeSpectrumEquivMaximalSpectrum_comp_asIdeal`, `MaximalSpectrum.toPiLocalization_not_surjective_of_infinite`, `PrimeSpectrum.piLocalizationToMaximal_bijective`, `IsArtinianRing.primeSpectrumEquivMaximalSpectrum_symm_comp_asIdeal`, `IsArtinianRing.instFiniteMaximalSpectrum`, `PrimeSpectrum.maximalSpectrumToPiLocalization_surjective_of_discreteTopology`, `MaximalSpectrum.instNonemptyOfNontrivial`

---

← Back to Index