restrictScalars — Mathlib

English

If T is symmetric, then its real-restricted form T.restrictScalars ℝ is symmetric.

Русский

Если T симметричен, то его ограничение по действительным скалярам T.restrictScalars ℝ симметрично.

LaTeX

$$$ (T.restrictScalars \mathbb{R}).IsSymmetric$$$

Lean4

theorem restrictScalars {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) :
    letI := InnerProductSpace.rclikeToReal 𝕜 E
    letI : IsScalarTower ℝ 𝕜 E := RestrictScalars.isScalarTower _ _ _
    (T.restrictScalars ℝ).IsSymmetric :=
  fun x y => by simp [hT x y, real_inner_eq_re_inner, LinearMap.coe_restrictScalars ℝ]

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