sub_of_commute

Mathlib.LinearAlgebra.Semisimple

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

← MathLib Explorer

English

If f and g commute and are semisimple, then f − g is semisimple.

Русский

Если f и g коммютируют и семисемпсимы, то f − g семисемпсим.

LaTeX

$$$ Commute(f,g) \land IsSemisimple(f) \land IsSemisimple(g) \Rightarrow IsSemisimple(f-g)$$$

Lean4

theorem sub_of_commute : (f - g).IsSemisimple :=
  .of_mem_adjoin_pair comm hf hg <| sub_mem (Algebra.subset_adjoin <| .inl rfl) (Algebra.subset_adjoin <| .inr rfl)

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

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

Разделы

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

Аффилиация

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