English
For z ∈ ℂ, the linear map of left multiplication by z on the complex plane, written in the basis {1, i}, is represented by the 2×2 real matrix with entries [[Re(z), -Im(z)], [Im(z), Re(z)]].
Русский
Для z ∈ ℂ линейное отображение левого умножения на z в базисе {1, i} задаётся матрицей [[Re(z), -Im(z)], [Im(z), Re(z)]] и представляет собой матрицу левая умножения.
LaTeX
$$$\\mathrm{LeftMulMatrix}_{\\mathbb{R}}(z) = \\begin{pmatrix} \\operatorname{Re}(z) & -\\operatorname{Im}(z) \\\\ \\operatorname{Im}(z) & \\operatorname{Re}(z) \\end{pmatrix}$$$
Lean4
theorem leftMulMatrix_complex (z : ℂ) : Algebra.leftMulMatrix Complex.basisOneI z = !![z.re, -z.im; z.im, z.re] :=
by
ext i j
rw [Algebra.leftMulMatrix_eq_repr_mul, Complex.coe_basisOneI_repr, Complex.coe_basisOneI, mul_re, mul_im,
Matrix.of_apply]
fin_cases j <;> dsimp only [Fin.zero_eta, Fin.mk_one, Matrix.cons_val]
· simp only [one_re, mul_one, one_im, mul_zero, sub_zero, zero_add]
fin_cases i <;> rfl
· simp only [I_re, mul_zero, I_im, mul_one, zero_sub, add_zero]
fin_cases i <;> rfl
