conjTranspose_vecMulVec — Mathlib

English

If w ∈ α^m and v ∈ α^n, then the conjugate transpose of the outer product vecMulVec w v equals the outer product of star v and star w: (vecMulVec w v)^H = vecMulVec(v^*, w^*).

Русский

Если w ∈ α^m и v ∈ α^n, то сопряженное транспонирование внешнего произведения vecMulVec w v равно внешнему произведению vecMulVec(звездочка v, звездочка w).

LaTeX

$$$ (\mathrm{vecMulVec}(w,v))^{H} = \mathrm{vecMulVec}(v^{*}, w^{*}) $$$

Lean4

@[simp]
theorem conjTranspose_vecMulVec [Mul α] [StarMul α] (w : m → α) (v : n → α) :
    (vecMulVec w v)ᴴ = vecMulVec (star v) (star w) :=
  ext fun _ _ => star_mul _ _

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