Mathlib Changelog
v4
Changelog
About
Github
Theorem
IsSemiprimaryRing.finite_of_isNoetherian
Modification history
2025-02-25 14:06
Mathlib/RingTheory/HopkinsLevitzki.lean
feat(RingTheory): Artinian rings over Jacobson rings (#21904)
Added
IsSemiprimaryRing.finite_of_isNoetherian
View on Github →