star_vec_dotProduct_vec — Mathlib

English

The dot product of star(vec A) with vec B equals the trace of A^H B: star(vec A) · vec B = tr(A^H B).

Русский

Скалярное произведение star(vec A) и vec B равно следу от A^H B.

LaTeX

$$$$\operatorname{star}(\operatorname{vec}(A)) \cdot \operatorname{vec}(B) = \operatorname{trace}(A^{\mathrm{H}} B)$$$$

Lean4

theorem star_vec_dotProduct_vec [AddCommMonoid R] [Mul R] [Star R] [Fintype m] [Fintype n] (A B : Matrix m n R) :
    star (vec A) ⬝ᵥ vec B = (Aᴴ * B).trace := by
  simp_rw [star_vec, vec_dotProduct_vec, ← conjTranspose_transpose, transpose_transpose]

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