toMatrix_conjAe — Mathlib

English

The matrix of conjAe in the basis {1, i} is the diagonal matrix diag(1, -1).

Русский

Матрица conjAe в базисе {1, i} равна диагональной матрице diag(1, -1).

LaTeX

$$$ \text{toMatrix}_{basisOneI,basisOneI}(conjAe\,\text{toLinearMap}) = \begin{pmatrix}1 & 0 \\ 0 & -1\end{pmatrix}. $$$

Lean4

/-- The matrix representation of `conjAe`. -/
@[simp]
theorem toMatrix_conjAe : LinearMap.toMatrix basisOneI basisOneI conjAe.toLinearMap = !![1, 0; 0, -1] :=
  by
  ext i j
  fin_cases i <;> fin_cases j <;> simp [LinearMap.toMatrix_apply]

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