mulVec_conjTranspose — Mathlib

English

The conjugate transpose interacts with vecMul: Aᴴ *ᵥ x = star (star x ᵥ* A).

Русский

Сопряжённое транспонирование взаимодействует с vecMul: Aᴴ *ᵥ x = star (star x ᵥ* A).

LaTeX

$$$A^{\\mathsf{H}} *\\!\\!\\!\\mathrm{vec} x = \\operatorname{star}(\\operatorname{vecMul}(\\operatorname{star} x, A))$$$

Lean4

theorem mulVec_conjTranspose [Fintype m] [StarRing α] (A : Matrix m n α) (x : m → α) : Aᴴ *ᵥ x = star (star x ᵥ* A) :=
  funext fun _ => star_dotProduct _ _

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