conjTranspose_apply — Mathlib

English

For any matrix M, the (j,i)-entry of M^H is the complex conjugate of the (i,j)-entry of M: (M^H)_{j i} = \overline{M_{i j}}.

Русский

Для любой матрицы M элемент (j,i) в M^H равен комплексному сопряжению элемента (i,j) в M: (M^H)_{j i} = \overline{M_{i j}}.

LaTeX

$$$ (M^{H})_{j i} = \overline{M_{i j}} $$$

Lean4

/-- Tell `simp` what the entries are in a conjugate transposed matrix.

  Compare with `mul_apply`, `diagonal_apply_eq`, etc.
-/
@[simp]
theorem conjTranspose_apply [Star α] (M : Matrix m n α) (i j) : M.conjTranspose j i = star (M i j) :=
  rfl

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