invFun_algebraMap — Mathlib

English

The matrix equivalence applied to a single-entry matrix equals the tensor of that entry with a unit block.

Русский

Применение эквивалентности к единичной блочной матрице даёт тензор одной величины с единичным блоком.

LaTeX

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

Lean4

@[simp]
theorem invFun_algebraMap (M : Matrix n n R) : invFun n R A (M.map (algebraMap R A)) = 1 ⊗ₜ M :=
  by
  dsimp [invFun]
  simp only [Algebra.algebraMap_eq_smul_one, smul_tmul, ← tmul_sum]
  congr
  conv_rhs => rw [matrix_eq_sum_single M]
  convert Finset.sum_product (β := Matrix n n R) ..; simp

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