mul_of_commute

Mathlib.LinearAlgebra.Semisimple

URI: https://scilib.ai/kg/mathlib#Module.End.IsSemisimple.mul_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\cdot g)$$$

Lean4

theorem mul_of_commute : (f * g).IsSemisimple :=
  .of_mem_adjoin_pair comm hf hg <| mul_mem (Algebra.subset_adjoin <| .inl rfl) (Algebra.subset_adjoin <| .inr rfl)

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

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

Разделы

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

Аффилиация

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