trace_replicateCol_mul_replicateRow

English

For a function a: n→R and b: n→R, tr(replicateColι a · replicateRowι b) = a ⬝ᵥ b (dot product).

Русский

Для функций a и b: tr(replicateColι a · replicateRowι b) = a ⬝ᵥ b (скалярное произведение).

LaTeX

$$$$ \operatorname{tr}( \operatorname{replicateCol}_{\iota} a \; \operatorname{replicateRow}_{\iota} b ) = a \cdot b $$$$

Lean4

@[simp]
theorem trace_replicateCol_mul_replicateRow {ι : Type*} [Unique ι] [NonUnitalNonAssocSemiring R] (a b : n → R) :
    trace (replicateCol ι a * replicateRow ι b) = a ⬝ᵥ b :=
  by
  apply Finset.sum_congr rfl
  simp [mul_apply]

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