instIsSemisimpleRingAddMonoidAlgebra

English

For a finite group G and a field k, the group algebra AddMonoidAlgebra k G is semisimple; consequently every MonoidAlgebra k G-module V is semisimple, i.e., is a direct sum of simple submodules.

Русский

Для конечной группы G и поля k алгебра группы AddMonoidAlgebra k G семисемпсиальна; следовательно, каждый модуль MonoidAlgebra k G над V распадается на прямую сумму простых подмодулей.

LaTeX

$$$\text{IsSemisimpleModule } (MonoidAlgebra k G) V$$$

Lean4

instance [AddGroup G] : IsSemisimpleRing (AddMonoidAlgebra k G) :=
  haveI : NeZero (Fintype.card (Multiplicative G) : k) := by rwa [Fintype.card_congr Multiplicative.toAdd]
  (AddMonoidAlgebra.toMultiplicativeAlgEquiv k G (R := ℕ)).toRingEquiv.symm.isSemisimpleRing

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