smulTower_leftMulMatrix_algebraMap_ne

English

For the smulTower construction in a tower of algebras, the left multiplication matrix evaluated at an algebra map with distinct indices k ≠ k' yields zero.

Русский

Для конструкции smulTower в цепочке альгебр, левая матрица умножения, применённая к алгебраическому отображению и к разным индексам k ≠ k', даёт ноль.

LaTeX

$$$ leftMulMatrix (b.smulTower c) (algebraMap _ _ x) (i, k) (j, k') = 0 \\; \\text{ при } k \\neq k' $$$

Lean4

theorem smulTower_leftMulMatrix_algebraMap_ne (x : S) (i j) {k k'} (h : k ≠ k') :
    leftMulMatrix (b.smulTower c) (algebraMap _ _ x) (i, k) (j, k') = 0 := by
  rw [smulTower_leftMulMatrix_algebraMap, blockDiagonal_apply_ne _ _ _ h]

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