isSemisimple_id — Mathlib

English

If M is semisimple as an R-module, then the identity endomorphism is semisimple.

Русский

Если M является семисимплексным как R-модуль, тождественный эндоморфизм композиции является семисимплексным.

LaTeX

$$$$ [IsSemisimpleModule\\ R\\ M] \\Rightarrow IsSemisimple\\ (LinearMap.id : Module.End\\ R\\ M). $$$$

Lean4

@[simp]
theorem isSemisimple_id [IsSemisimpleModule R M] : IsSemisimple (LinearMap.id : Module.End R M) := by
  simpa [isSemisimple_iff] using exists_isCompl

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