blockDiagonal_pow — Mathlib

English

BlockDiagonal respects powers: blockDiagonal(M^n) = (blockDiagonal M)^n for finite index sets and semiring structure.

Русский

BlockDiagonal сохраняет степени: blockDiagonal(M^n) = (blockDiagonal M)^n для конечных индексов и полей полусложения.

LaTeX

$$$\operatorname{blockDiagonal}(M^{n}) = (\operatorname{blockDiagonal}M)^{n}.$$$

Lean4

@[simp]
theorem blockDiagonal_pow [DecidableEq m] [Fintype o] [Fintype m] [Semiring α] (M : o → Matrix m m α) (n : ℕ) :
    blockDiagonal (M ^ n) = blockDiagonal M ^ n :=
  map_pow (blockDiagonalRingHom m o α) M n

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