isFinitelySemisimple

Mathlib.LinearAlgebra.Semisimple

URI: https://scilib.ai/kg/mathlib#Module.End.IsSemisimple.isFinitelySemisimple

English

For End_R(M) with M finite over R, IsFinitelySemisimple is equivalent to IsSemisimple.

Русский

Для End_R(M) при конечномерности M над R IsFinitelySemisimple эквивалично IsSemisimple.

LaTeX

$$$ [\ ModuleFinite R M] \ Rightarrow (IsFinitelySemisimple(f) \iff IsSemisimple(f))$$$

Lean4

theorem isFinitelySemisimple (hf : f.IsSemisimple) : f.IsFinitelySemisimple :=
  isFinitelySemisimple_iff'.mp fun _ _ _ ↦ hf.restrict _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru