isSemisimple_neg

Mathlib.LinearAlgebra.Semisimple

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

English

(-f) is semisimple iff f is semisimple.

Русский

(-f) семисимплексен тогда и только тогда, когда f семисимплексен.

LaTeX

$$$$ (-f).IsSemisimple \\iff f.IsSemisimple. $$$$

Lean4

@[simp]
theorem isSemisimple_neg : (-f).IsSemisimple ↔ f.IsSemisimple := by simp [isSemisimple_iff, mem_invtSubmodule]

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

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

Разделы

Аффилиация

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