Structures · Algebra
IsSemiprimaryRing
A ring is semiprimary if its Jacobson radical is nilpotent and its quotient by the Jacobson radical is semisimple.
- Defined in
- Mathlib.RingTheory.Jacobson.Semiprimary
- Shape
- One type argument · adds isSemisimpleRing, isNilpotent
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by8
- IsSemiprimaryRing.induction
- IsSemiprimaryRing.isNoetherian_iff_isArtinian
- IsSemiprimaryRing.isNoetherian_iff_finite_of_jacobson_fg
- IsSemiprimaryRing.isNilpotent
- IsSemiprimaryRing.finite_of_isArtinian
- IsSemiprimaryRing.isNoetherianRing_iff_jacobson_fg
- IsSemiprimaryRing.finite_of_isNoetherian
- IsSemiprimaryRing.isSemisimpleRing
Ancestors0
No ancestors.