conjTranspose_mul — Mathlib

English

Let M be an m×n matrix and N an n×l matrix with entries in α. The conjugate transpose reverses the order of multiplication: (M N)^H = N^H M^H.

Русский

Пусть M — матрица размера m×n, N — матрица размера n×l над α. Конъюгированное транспонирование обращает порядок умножения: (M N)^H = N^H M^H.

LaTeX

$$$ (M N)^H = N^H M^H $$$

Lean4

@[simp]
theorem conjTranspose_mul [Fintype n] [NonUnitalNonAssocSemiring α] [StarRing α] (M : Matrix m n α) (N : Matrix n l α) :
    (M * N)ᴴ = Nᴴ * Mᴴ :=
  Matrix.ext <| by simp [mul_apply]

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