instFiniteElemSubmoduleIsotypicComponentsOfIsNoetherian

English

If M is a Noetherian module over R, then the set of isotypic components is finite.

Русский

Если M является конечноподобным (Noetherian) модулем над R, то множество изотипических компонентов конечное.

LaTeX

$$$$ \\text{If } M \\text{ is Noetherian over } R, \\; \\mathrm{isotypicComponents}(R,M) \\, \\text{is finite}. $$$$

Lean4

instance [IsNoetherian R M] : Finite (isotypicComponents R M) :=
  Set.finite_coe_iff.mpr <| WellFoundedGT.finite_of_sSupIndep (sSupIndep_isotypicComponents R M)

Похожие утверждения