smulTower_leftMulMatrix_algebraMap_eq

English

A refined equality for tower left multiplication with algebra map on x.

Русский

Уточненное равенство башенного левого умножения с алгебраической картой на x.

LaTeX

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

Lean4

theorem smulTower_leftMulMatrix_algebraMap_eq (x : S) (i j k) :
    leftMulMatrix (b.smulTower c) (algebraMap _ _ x) (i, k) (j, k) = leftMulMatrix b x i j := by
  rw [smulTower_leftMulMatrix_algebraMap, blockDiagonal_apply_eq]

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