instIsSemisimpleModule — Mathlib

English

Let p be a submodule of MonoidAlgebra k G acting on V. Then there exists a submodule q such that p and q are complementary: p ⊔ q = V and p ∩ q = {0} (IsCompl).

Русский

Пусть p — подмодуль MonoidAlgebra k G, действующий на V. Тогда существует подмодуль q, такой что p и q образуют разложение в прямую сумму: p ⊕ q = V и p ∩ q = {0}.

LaTeX

$$$\exists q : Submodule (MonoidAlgebra k G) V, IsCompl p q$$$

Lean4

/-- This also implies instances `ComplementedLattice (Submodule (MonoidAlgebra k G) V)` and
`IsSemisimpleRing (MonoidAlgebra k G)`. -/
instance : IsSemisimpleModule (MonoidAlgebra k G) V where exists_isCompl := exists_isCompl

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