matrixEquivTensor_apply_symm — Mathlib

English

The specialized form of matrixEquivTensor on a single entry yields the simple tensor form: matrixEquivTensor(single i j x) = x ⊗ single i j 1.

Русский

Специализированная форма matrixEquivTensor на один элемент даёт простую форму тензора: matrixEquivTensor(single i j x) = x ⊗ single i j 1.

LaTeX

$$$ matrixEquivTensor(n,R,A)(single\; i\; j\; x) = x \otimes_\mathrm{T} single(i,j,1) $$$

Lean4

@[simp]
theorem matrixEquivTensor_apply_symm (a : A) (M : Matrix n n R) :
    (matrixEquivTensor n R A).symm (a ⊗ₜ M) = a • M.map (algebraMap R A) :=
  rfl

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