IsSemisimple — Mathlib

English

IsSemisimple is defined as the semisimplicity of the induced R[X]-module structure on M via AEval' f.

Русский

IsSemisimple задаётся как полная структурная полная развёрнутость модуля M над кольцом R[X] через действие AEval' f.

LaTeX

$$$$ \\text{IsSemisimple}(f) \\iff \\text{IsSemisimpleModule}(R[X],\\ AEval'(f)). $$$$

Lean4

/-- A linear endomorphism of an `R`-module `M` is called *semisimple* if the induced `R[X]`-module
structure on `M` is semisimple. This is equivalent to saying that every `f`-invariant `R`-submodule
of `M` has an `f`-invariant complement: see `Module.End.isSemisimple_iff`. -/
def IsSemisimple :=
  IsSemisimpleModule R[X] (AEval' f)

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