Finitely generated modules over an Artinian ring have finite length

A finitely generated module over a left Artinian ring has finite length, which is one implication of Mathlib's IsArtinianRing.tfae. The ring need not be commutative. The same holds over the base of any finite extension, in particular for a finitely generated module over an Artin algebra.

theorem TauCeti.isFiniteLength_of_finite (R : Type u) [Ring R] [IsArtinianRing R] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] : IsFiniteLength R M

A finitely generated module over an Artinian ring has finite length.

theorem TauCeti.isFiniteLength_of_finite_trans (R : Type u) [Ring R] [IsArtinianRing R] (B : Type v) [Semiring B] [Module R B] [Module.Finite R B] (M : Type w) [AddCommGroup M] [Module R M] [Module B M] [IsScalarTower R B M] [Module.Finite B M] : IsFiniteLength R M

A module that is finitely generated over a finite extension B of an Artinian ring R, such as an Artin R-algebra, has finite length over R.