conjTranspose_kronecker — Mathlib

English

The conjugate transpose distributes over Kronecker product: (x ⊗ y)^H = x^H ⊗ y^H, for matrices over a commutative magma with star.

Русский

Сопряжённое преобразование распределяется по Кронеcker: (x ⊗ y)^H = x^H ⊗ y^H для матриц над коммутативной структурой с операцией сопряжения.

LaTeX

$$$$ (x \\otimes y)^H = x^H \\otimes y^H $$$$

Lean4

theorem conjTranspose_kronecker [CommMagma R] [StarMul R] (x : Matrix l m R) (y : Matrix n p R) :
    (x ⊗ₖ y)ᴴ = xᴴ ⊗ₖ yᴴ := by ext; simp

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