smulTower_leftMulMatrix_algebraMap

English

The left multiplication matrix over a tower equals the block diagonal of left multiplications by x.

Русский

Левая матрица умножения через башню эквивалентна блочной диагонали левых умножений на x.

LaTeX

$$$\text{smulTower_leftMulMatrix_algebraMap_eq}(b,c,x,i,j) :\; \text{leftMulMatrix}(b.smulTower c)(\text{algebraMap } x)_{(i,j)} = \text{leftMulMatrix}(b)\; x_{i j}.$$$

Lean4

theorem smulTower_leftMulMatrix_algebraMap (x : S) :
    leftMulMatrix (b.smulTower c) (algebraMap _ _ x) = blockDiagonal fun _ ↦ leftMulMatrix b x :=
  by
  ext ⟨i, k⟩ ⟨j, k'⟩
  rw [smulTower_leftMulMatrix, AlgHom.commutes, blockDiagonal_apply, algebraMap_matrix_apply]
  split_ifs with h <;> simp only at h <;> simp

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