conjTranspose_kronecker' — Mathlib

English

A version with matrix reversal symmetry: (x ⊗ₖ y)ᴴ = (yᴴ ⊗ₖ xᴴ).submatrix Prod.swap Prod.swap.

Русский

Версия с симметрией разворота: (x ⊗ₖ y)ᴴ = (yᴴ ⊗ₖ xᴴ).submatrix Prod.swap Prod.swap.

LaTeX

$$$ (x \otimes_k y)^{\mathrm{H}} = (y^{\mathrm{H}} \otimes_k x^{\mathrm{H}}).submatrix(\mathrm{Prod.swap}) (\mathrm{Prod.swap}) $$$

Lean4

theorem conjTranspose_kronecker' [Mul R] [StarMul R] (x : Matrix l m R) (y : Matrix n p R) :
    (x ⊗ₖ y)ᴴ = (yᴴ ⊗ₖ xᴴ).submatrix Prod.swap Prod.swap := by ext; simp

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