isotypicComponent — Mathlib

English

If M is the direct sum of fully invariant submodules N_i indexed by a set, then End_R(M) is isomorphic to the product of End_R(N_i) as algebras.

Русский

Если M является прямой суммой полностью инвариантных подподмодулей N_i индексируемых i по некоторому множеству, то End_R(M) изоморфно произведению End_R(N_i) как алгебры.

LaTeX

$$$$ \\mathrm{End}_R(M) \\cong \\prod_i \\mathrm{End}_R(N_i). $$$$

Lean4

protected theorem isotypicComponent : (isotypicComponent R M S).IsFullyInvariant :=
  LinearMap.le_comap_isotypicComponent S

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