Documentation Verification Report

Module

📁 Source: Mathlib/RingTheory/Spectrum/Prime/Module.lean

Statistics

Metric	Count
Definitions	0
Theorems `closedPoint_mem_support`, `subsingleton_iff_disjoint`, `isClosed_support`, `stableUnderSpecialization_support`, `support_subset_preimage_comap`	5
Total	5

IsLocalRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closedPoint_mem_support` 📖	mathematical	—	`PrimeSpectrum` `CommRing.toCommSemiring` `Set` `Set.instMembership` `Module.support` `closedPoint`	—	`Module.nonempty_support_iff` `Module.mem_support_mono` `le_top`

LocalizedModule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`subsingleton_iff_disjoint` 📖	mathematical	—	`LocalizedModule` `CommRing.toCommSemiring` `Submonoid.powers` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `AddCommGroup.toAddCommMonoid` `Disjoint` `Set` `PrimeSpectrum` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `SetLike.coe` `TopologicalSpace.Opens` `PrimeSpectrum.zariskiTopology` `TopologicalSpace.Opens.instSetLike` `PrimeSpectrum.basicOpen` `Module.support`	—	`subsingleton_iff_support_subset` `PrimeSpectrum.basicOpen_eq_zeroLocus_compl` `disjoint_compl_left_iff` `Set.le_iff_subset`

Module

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isClosed_support` 📖	mathematical	—	`IsClosed` `PrimeSpectrum` `CommRing.toCommSemiring` `PrimeSpectrum.zariskiTopology` `support`	—	`support_eq_zeroLocus` `PrimeSpectrum.isClosed_zeroLocus`
`stableUnderSpecialization_support` 📖	mathematical	—	`StableUnderSpecialization` `PrimeSpectrum` `CommRing.toCommSemiring` `PrimeSpectrum.zariskiTopology` `support`	—	`mem_support_mono` `PrimeSpectrum.le_iff_specializes`
`support_subset_preimage_comap` 📖	mathematical	—	`Set` `PrimeSpectrum` `CommRing.toCommSemiring` `Set.instHasSubset` `support` `Set.preimage` `PrimeSpectrum.comap` `algebraMap` `CommSemiring.toSemiring`	—	`RingHom.instRingHomClass` `algebraMap_smul`

---

← Back to Index