IsSemisimple_smul_iff

Mathlib.LinearAlgebra.Semisimple

URI: https://scilib.ai/kg/mathlib#Module.End.IsSemisimple_smul_iff

← MathLib Explorer

English

For t ≠ 0, (t · f).IsSemisimple ⇔ f.IsSemisimple.

Русский

Для t ≠ 0, (t · f).IsSemisimple ⇔ f.IsSemisimple.

LaTeX

$$$ {t \neq 0} \Rightarrow (t \cdot f).IsSemisimple \iff f.IsSemisimple$$$

Lean4

theorem IsSemisimple_smul_iff {t : K} (ht : t ≠ 0) : (t • f).IsSemisimple ↔ f.IsSemisimple := by
  simp [isSemisimple_iff, mem_invtSubmodule, Submodule.comap_smul f (h := ht)]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru