English
restrictScalars with respect to ℝ of the ℂ-action decomposes as the sum of real and imaginary parts: reCLM.smulRight x + i · imCLM.smulRight x.
Русский
restrictScalars относительно ℝ от ℂ-действия разложимо на сумму действительной и мнимой частей: reCLM.smulRight x + i · imCLM.smulRight x.
LaTeX
$$$$ \\operatorname{restrictScalars}_{\\mathbb{R}} \\left( (1 : \\mathbb{C} \\to_L^{\\mathbb{C}} \\mathbb{C}).\\mathrm{smulRight} x \\right) = \\mathrm{reCLM}.\\mathrm{smulRight} x + i \\cdot \\mathrm{imCLM}.\\mathrm{smulRight} x. $$$$
Lean4
theorem restrictScalars_one_smulRight' (x : E) :
ContinuousLinearMap.restrictScalars ℝ ((1 : ℂ →L[ℂ] ℂ).smulRight x : ℂ →L[ℂ] E) =
reCLM.smulRight x + I • imCLM.smulRight x :=
by
ext ⟨a, b⟩
simp [map_add, mk_eq_add_mul_I, mul_smul, smul_comm I b x]
