English
The dot product of vec A and vec B equals the trace of A^T B: vec(A) · vec(B) = tr(A^T B).
Русский
Скалярное произведение vec(A) и vec(B) равно следу от A^T B: vec(A)·vec(B) = tr(A^T B).
LaTeX
$$$$\operatorname{vec}(A) \cdot \operatorname{vec}(B) = \operatorname{trace}(A^{\top} B)$$$$
Lean4
theorem vec_dotProduct_vec [AddCommMonoid R] [Mul R] [Fintype m] [Fintype n] (A B : Matrix m n R) :
vec A ⬝ᵥ vec B = (Aᵀ * B).trace := by
simp_rw [Matrix.trace, Matrix.diag, Matrix.mul_apply, dotProduct, vec, transpose_apply, ← Finset.univ_product_univ,
Finset.sum_product]