restrictScalars_one_smulRight — Mathlib

English

For x ∈ ℂ, restrictScalars ℝ ((1 : ℂ →L[ℂ] ℂ).smulRight x) = x • (1 : ℂ →L[ℝ] ℂ).

Русский

Для x ∈ ℂ, restrictScalars ℝ ((1 : ℂ →L[ℂ] ℂ).smulRight x) = x • (1 : ℂ →L[ℝ] ℂ).

LaTeX

$$$$ \\operatorname{restrictScalars}_{\\mathbb{R}}\\bigl((1 : \\mathbb{C} \\to_L^{\\mathbb{C}} \\mathbb{C}).\\mathrm{smulRight} x\\bigr) = x \\cdot \\bigl(1 : \\mathbb{C} \\to_L^{\\mathbb{R}} \\mathbb{C}\\bigr). $$$$

Lean4

theorem restrictScalars_one_smulRight (x : ℂ) :
    ContinuousLinearMap.restrictScalars ℝ ((1 : ℂ →L[ℂ] ℂ).smulRight x : ℂ →L[ℂ] ℂ) = x • (1 : ℂ →L[ℝ] ℂ) :=
  by
  ext1 z
  dsimp
  apply mul_comm

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