vec_dotProduct_vec — Mathlib

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]

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