English
If a real-linear map ℓ: ℂ →ℝ E satisfies ℓ(i) = i · ℓ(1), then ℓ(a b) = a ℓ(b) for all a,b ∈ ℂ.
Русский
Если вещественно-линейная карта ℓ: ℂ →ℝ E удовлетворяет ℓ(i) = i · ℓ(1), тогда для любых a,b ∈ ℂ имеет место ℓ(a b) = a ℓ(b).
LaTeX
$$$\forall a,b \in \mathbb{C}, \ \ell(a b) = a \ell(b)$ given $\ell(i) = i \ell(1)$$$
Lean4
/-- A real linear map `ℓ : ℂ →ₗ[ℝ] E` respects complex scalar multiplication if it maps `I` to
`I • ℓ 1`.
-/
theorem real_linearMap_map_smul_complex {ℓ : ℂ →ₗ[ℝ] E} (h : ℓ I = I • ℓ 1) (a b : ℂ) : ℓ (a • b) = a • ℓ b :=
by
rw [← re_add_im a, ← re_add_im b, ← smul_eq_mul _ I, ← smul_eq_mul _ I]
have t₀ : ((a.im : ℂ) • I) • (b.re : ℂ) = (↑(a.im * b.re) : ℂ) • I := by
simp only [smul_eq_mul, ofReal_mul, ← mul_assoc, mul_comm _ I]
have t₁ : ((a.im : ℂ) • I) • (b.im : ℂ) • I = (↑(-a.im * b.im) : ℂ) • (1 : ℂ) := by simp [mul_mul_mul_comm _ I]
simp only [add_smul, smul_add, ℓ.map_add, t₀, t₁]
repeat rw [Complex.coe_smul, ℓ.map_smul]
have t₂ {r : ℝ} : ℓ (r : ℂ) = r • ℓ (1 : ℂ) := by simp [← ℓ.map_smul]
simp only [t₂, h]
match_scalars
simp [mul_mul_mul_comm _ I]
ring
