Documentation Verification Report

Compact

📁 Source: Mathlib/Topology/Algebra/Ring/Compact.lean

Statistics

Metric	Count
Definitions	0
Theorems `isOpen_of_isMaximal`, `isOpen_pow_of_isMaximal`, `finite_of_compactSpace_of_t2Space`, `isOpen_iff`, `isOpen_of_ne_bot`, `isOpen_iff`, `finite_residueField_of_compactSpace`, `isOpen_iff_finite_quotient`, `isOpen_maximalIdeal`, `isOpen_maximalIdeal_pow`, `instFiniteQuotientIdealOfIsMaximal`	11
Total	11

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isOpen_of_isMaximal` 📖	mathematical	—	`IsOpen` `SetLike.coe` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`AddSubgroup.finiteIndex_of_finite_quotient` `AddSubgroup.isOpen_of_isClosed_of_finiteIndex` `instSeparatelyContinuousAddOfContinuousAdd` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing`
`isOpen_pow_of_isMaximal` 📖	mathematical	—	`IsOpen` `SetLike.coe` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.instPowNat` `IsScalarTower.right` `Algebra.id`	—	`IsScalarTower.right` `AddSubgroup.finiteIndex_of_finite_quotient` `finite_quotient_pow` `IsNoetherian.noetherian` `DivisionRing.finite_of_compactSpace_of_t2Space` `topologicalRing_quotient` `instCompactSpaceQuotientIdeal` `T25Space.t2Space` `T3Space.t25Space` `Submodule.t3_quotient_of_isClosed` `IsSemitopologicalRing.toIsTopologicalAddGroup` `IsTopologicalRing.toIsSemitopologicalRing` `IsNoetherianRing.isClosed_ideal` `AddSubgroup.isOpen_of_isClosed_of_finiteIndex` `instSeparatelyContinuousAddOfContinuousAdd` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsCompact.isClosed` `isCompact_of_fg` `IsTopologicalRing.toIsTopologicalSemiring`

IsArtinianRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_of_compactSpace_of_t2Space` 📖	mathematical	—	`Finite`	—	`IsScalarTower.left` `isNilpotent_jacobson_bot` `IsScalarTower.right` `instFinitePrimeSpectrum` `le_bot_iff` `Ideal.zero_eq_bot` `pow_le_pow_left₀` `IsOrderedRing.toPosMulMono` `Submodule.instIsOrderedRing` `IsOrderedRing.toMulPosMono` `zero_le` `Submodule.instCanonicallyOrderedAdd` `Ideal.jacobson_bot` `Ring.jacobson_eq_sInf_isMaximal` `le_sInf_iff` `LE.le.trans` `Ideal.prod_le_inf` `Finset.inf_le` `Ideal.IsMaximal.isPrime` `Ideal.finite_quotient_prod` `IsNoetherian.noetherian` `instIsNoetherianRingOfIsArtinianRing` `DivisionRing.finite_of_compactSpace_of_t2Space` `isMaximal_of_isPrime` `PrimeSpectrum.isPrime` `topologicalRing_quotient` `instCompactSpaceQuotientIdeal` `T25Space.t2Space` `T3Space.t25Space` `Submodule.t3_quotient_of_isClosed` `IsSemitopologicalRing.toIsTopologicalAddGroup` `IsTopologicalRing.toIsSemitopologicalRing` `IsNoetherianRing.isClosed_ideal` `Ideal.finite_quotient_pow` `Finite.of_equiv` `Ideal.instIsTwoSidedBot`

IsDedekindDomain

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isOpen_iff` 📖	mathematical	`IsField` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`IsOpen` `SetLike.coe` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`discreteTopology_iff_isOpen_singleton_zero` `instSeparatelyContinuousAddOfContinuousAdd` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `Finite.isField_of_domain` `toIsDomain` `finite_of_compact_of_discrete` `isOpen_of_ne_bot`
`isOpen_of_ne_bot` 📖	mathematical	—	`IsOpen` `SetLike.coe` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`Ideal.finprod_heightOneSpectrum_factorization` `Ideal.hasFiniteMulSupport` `finprod_eq_finset_prod_of_mulSupport_subset` `Set.Finite.coe_toFinset` `Set.instReflSubset` `AddSubgroup.isOpen_of_isClosed_of_finiteIndex` `instSeparatelyContinuousAddOfContinuousAdd` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `AddSubgroup.finiteIndex_of_finite_quotient` `Ideal.finite_quotient_prod` `IsNoetherian.noetherian` `IsDedekindDomainDvr.toIsNoetherian` `toIsDomain` `isDedekindDomainDvr` `Ideal.finite_quotient_pow` `DivisionRing.finite_of_compactSpace_of_t2Space` `HeightOneSpectrum.isMaximal` `topologicalRing_quotient` `instCompactSpaceQuotientIdeal` `T25Space.t2Space` `T3Space.t25Space` `Submodule.t3_quotient_of_isClosed` `IsSemitopologicalRing.toIsTopologicalAddGroup` `IsNoetherianRing.isClosed_ideal` `Ideal.uniqueFactorizationMonoid`

IsDiscreteValuationRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isOpen_iff` 📖	mathematical	—	`IsOpen` `SetLike.coe` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`IsDedekindDomain.isOpen_iff` `IsPrincipalIdealRing.isDedekindDomain` `toIsPrincipalIdealRing` `not_isField`

IsLocalRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_residueField_of_compactSpace` 📖	mathematical	—	`Finite` `ResidueField`	—	—
`isOpen_iff_finite_quotient` 📖	mathematical	—	`IsOpen` `SetLike.coe` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Finite` `HasQuotient.Quotient` `Ideal.instHasQuotient_1`	—	`AddSubgroup.quotient_finite_of_isOpen` `instSeparatelyContinuousAddOfContinuousAdd` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `exists_maximalIdeal_pow_le_of_isArtinianRing_quotient` `isArtinian_of_fg_of_artinian'` `Finite.to_wellFoundedLT` `Finite.of_fintype` `Module.Finite.self` `AddSubgroup.isOpen_mono` `IsScalarTower.right` `isOpen_maximalIdeal_pow`
`isOpen_maximalIdeal` 📖	mathematical	—	`IsOpen` `SetLike.coe` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `maximalIdeal`	—	`Ideal.isOpen_of_isMaximal` `maximalIdeal.isMaximal`
`isOpen_maximalIdeal_pow` 📖	mathematical	—	`IsOpen` `SetLike.coe` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.instPowNat` `IsScalarTower.right` `Algebra.id` `maximalIdeal`	—	`Ideal.isOpen_pow_of_isMaximal` `maximalIdeal.isMaximal`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instFiniteQuotientIdealOfIsMaximal` 📖	mathematical	—	`Finite` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1`	—	`DivisionRing.finite_of_compactSpace_of_t2Space` `topologicalRing_quotient` `instCompactSpaceQuotientIdeal` `T25Space.t2Space` `T3Space.t25Space` `Submodule.t3_quotient_of_isClosed` `IsSemitopologicalRing.toIsTopologicalAddGroup` `IsTopologicalRing.toIsSemitopologicalRing` `IsNoetherianRing.isClosed_ideal`

---

← Back to Index