Documentation Verification Report

Artinian

📁 Source: Mathlib/RingTheory/Jacobson/Artinian.lean

Statistics

Metric	Count
Definitions `Artinian`	1
Theorems `finite_iff_isArtinianRing`, `finite_iff_krullDimLE_zero`, `finite_of_isArtinianRing`, `finite_of_isSemisimpleRing`	4
Total	5

CategoryTheory

Definitions

Name	Category	Theorems
`Artinian` 📖	CompData	—

Module

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_iff_isArtinianRing` 📖	mathematical	—	`Finite` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `IsArtinianRing`	—	`isArtinian_of_tower` `IsScalarTower.right` `List.TFAE.out` `IsArtinianRing.tfae` `finite_of_isArtinianRing` `instIsJacobsonRingOfKrullDimLEOfNatNat` `PrimeSpectrum.instKrullDimLEOfNatNat`
`finite_iff_krullDimLE_zero` 📖	mathematical	—	`Finite` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `Ring.KrullDimLE`	—	`Algebra.FiniteType.isNoetherianRing` `instIsNoetherianRingOfIsArtinianRing` `finite_iff_isArtinianRing` `isArtinianRing_iff_isNoetherianRing_krullDimLE_zero`
`finite_of_isArtinianRing` 📖	mathematical	—	`Finite` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule`	—	`finite_of_isSemisimpleRing` `Algebra.FiniteType.quotient` `IsSemiprimaryRing.isSemisimpleRing` `IsArtinianRing.instIsSemiprimaryRing` `IsSemiprimaryRing.finite_of_isArtinian` `IsScalarTower.right`
`finite_of_isSemisimpleRing` 📖	mathematical	—	`Finite` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule`	—	`finite_of_finite_type_of_isJacobsonRing` `Algebra.FiniteType.quotient` `Finite.equiv` `Finite.pi` `IsArtinianRing.instFiniteMaximalSpectrum` `instIsArtinianOfIsSemisimpleModuleOfFinite` `Finite.self` `IsScalarTower.right` `RingHomInvPair.ids` `Pi.isScalarTower` `Ideal.Quotient.isScalarTower` `instIsReducedOfIsSemisimpleRing`

---

← Back to Index