blockDiagonal_smul — Mathlib

English

BlockDiagonal defines a ring homomorphism from a family of matrices to a block matrix, respecting addition and multiplication.

Русский

BlockDiagonal образует кольцевой гомоморфизм от семейства матриц к блочной матрице, сохраняющий сложение и умножение.

LaTeX

$$$\operatorname{blockDiagonalRingHom} : (o \to Matrix m m α) \to_* Matrix (m \times o) (m \times o) α$$$

Lean4

@[simp]
theorem blockDiagonal_smul {R : Type*} [Zero α] [SMulZeroClass R α] (x : R) (M : o → Matrix m n α) :
    blockDiagonal (x • M) = x • blockDiagonal M := by
  ext
  simp only [blockDiagonal_apply, Pi.smul_apply, smul_apply]
  split_ifs <;> simp

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