instIsArtinianOfIsSemisimpleModuleOfFinite

English

If M is a semisimple R-module and M is finite as an R-module, then M is Artinian.

Русский

Если M является полным разложением как R-модуль и конечен над R, то M является артиньяновым модулем.

LaTeX

$$$\\displaystyle \\big(\\text{IsSemisimpleModule } R M \\big) \\wedge \\big(\\text{Module.Finite } R M \\big) \\Rightarrow \\text{IsArtinian } R M$$$

Lean4

instance [IsSemisimpleModule R M] [Module.Finite R M] : IsArtinian R M :=
  (IsSemisimpleModule.finite_tfae.out 0 2).mp ‹_›

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