Documentation Verification Report

Semiprimary

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

Statistics

Metric	Count
Definitions `IsSemiprimaryRing`	1
Theorems `isNilpotent`, `isSemisimpleRing`, `jacobson_eq_bot`, `jacobson_le_annihilator`, `jacobson_le_ker`, `jacobson_eq_bot`, `jacobson_eq_bot`, `instIsReducedOfIsSemisimpleRing`, `isSemiprimaryRing_iff`	9
Total	10

IsSemiprimaryRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isNilpotent` 📖	mathematical	—	`IsNilpotent` `Ideal` `Ring.toSemiring` `Submodule.pointwiseZero` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.instPowNat` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Module.toDistribMulAction` `Ring.jacobson`	—	—
`isSemisimpleRing` 📖	mathematical	—	`IsSemisimpleRing` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `Ideal.instHasQuotient` `Ring.jacobson` `Ideal.Quotient.ring` `Ring.instIsTwoSidedJacobson`	—	—

IsSemisimpleModule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`jacobson_eq_bot` 📖	mathematical	—	`Module.jacobson` `Bot.bot` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instBot`	—	`RingHomInvPair.ids` `isSemisimpleModule_iff_exists_linearEquiv_dfinsupp` `RingHomCompTriple.ids` `Module.jacobson_eq_bot_of_injective` `RingHomSurjective.ids` `DFinsupp.injective_pi_lapply` `LinearEquiv.injective` `Module.jacobson_pi_eq_bot` `IsSimpleModule.jacobson_eq_bot`
`jacobson_le_annihilator` 📖	mathematical	—	`Ideal` `Ring.toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ring.jacobson` `Module.annihilator` `AddCommGroup.toAddCommMonoid`	—	`Module.mem_annihilator` `Module.le_comap_jacobson` `RingHomSurjective.ids` `jacobson_eq_bot`
`jacobson_le_ker` 📖	mathematical	—	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Module.jacobson` `LinearMap.ker`	—	`LE.le.trans` `Module.le_comap_jacobson` `jacobson_eq_bot`

IsSemisimpleRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`jacobson_eq_bot` 📖	mathematical	—	`Ring.jacobson` `Bot.bot` `Ideal` `Ring.toSemiring` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`IsSemisimpleModule.jacobson_eq_bot`

IsSimpleModule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`jacobson_eq_bot` 📖	mathematical	—	`Module.jacobson` `Bot.bot` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instBot`	—	`le_bot_iff` `sInf_le` `isCoatom_bot` `toIsSimpleOrder`

(root)

Definitions

Name	Category	Theorems
`IsSemiprimaryRing` 📖	CompData	2 math math: `IsArtinianRing.instIsSemiprimaryRing`, `isSemiprimaryRing_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsReducedOfIsSemisimpleRing` 📖	mathematical	—	`IsReduced` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`Eq.le` `IsSemisimpleRing.jacobson_eq_bot` `Ideal.mem_sInf` `Ideal.IsPrime.mem_of_pow_mem` `Ideal.IsMaximal.isPrime` `Ideal.isMaximal_def` `Ideal.zero_mem`
`isSemiprimaryRing_iff` 📖	mathematical	—	`IsSemiprimaryRing` `IsSemisimpleRing` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `Ideal.instHasQuotient` `Ring.jacobson` `Ideal.Quotient.ring` `Ring.instIsTwoSidedJacobson` `IsNilpotent` `Submodule.pointwiseZero` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.instPowNat` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Module.toDistribMulAction`	—	`Ring.instIsTwoSidedJacobson` `IsScalarTower.left`

---

← Back to Index