Commit 2026-04-28 15:42 3a9f51ff
View on Github →feat(RingTheory/Spectrum/Prime/Noetherian): rank of an Artinian ring over a field (#38182) This PR proves that the rank of an Artinian ring over a field is the sum of the ranks of the localizations. This will be applied in #37130 to prove the ramification-inertia formula (this is where the sum first shows up).