smul — Mathlib

English

If conj(c) = c (i.e., c is real), and T is symmetric, then c·T is symmetric.

Русский

Если сопряжение c равно c (т.е. c вещественно), и T симметрично, то c·T симметрично.

LaTeX

$$$ (c \cdot T).IsSymmetric $ if $ \overline{c} = c $ and $ T.IsSymmetric$$$

Lean4

@[aesop safe apply]
theorem smul {c : 𝕜} (hc : conj c = c) {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) : c • T |>.IsSymmetric :=
  by
  intro x y
  simp only [smul_apply, inner_smul_left, hc, hT x y, inner_smul_right]

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