matrixEquivTensor_apply — Mathlib

English

The canonical matrixEquivTensor applied to a matrix M equals the sum over pairs (i,j) of M_{ij} ⊗ single(i,j,1).

Русский

Каноническая матрица-эквивалентность matrixEquivTensor, примененная к матрице M, равна сумме по парам (i,j) значения M_{ij} ⊗ единичный элемент.

LaTeX

$$$ matrixEquivTensor(n,R,A)\,M = \sum_{(i,j)\in n\times n} M_{ij} \otimes_\mathrm{K} single(i,j,1) $$$

Lean4

@[simp]
theorem matrixEquivTensor_apply (M : Matrix n n A) :
    matrixEquivTensor n R A M = ∑ p : n × n, M p.1 p.2 ⊗ₜ single p.1 p.2 1 :=
  rfl

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