mul_of_commute — Mathlib

English

If S and T are symmetric and commute, then ST is symmetric.

Русский

Если S и T симметричны и commute, тогда ST симметричен.

LaTeX

$$$ (S T).IsSymmetric$ if $S.IsSymmetric$, $T.IsSymmetric$, and $Commute S T$$$

Lean4

@[aesop 30% apply]
theorem mul_of_commute {S T : E →ₗ[𝕜] E} (hS : S.IsSymmetric) (hT : T.IsSymmetric) (hST : Commute S T) :
    (S * T).IsSymmetric := fun _ _ ↦ by rw [Module.End.mul_apply, hS, hT, hST, Module.End.mul_apply]

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