blockDiag_map — Mathlib

English

Applying a pointwise map f to M and then block-diagonalizing equals taking blockDiag of M and then applying f blockwise.

Русский

Применение отображения на элементы M до блочной диагонализации эквивалентно блочной диагонализации M с применением того же отображения по каждому блоку.

LaTeX

$$$ blockDiag (M.map f) = \lambda k. (blockDiag M k).map f $$$

Lean4

theorem blockDiag_map (M : Matrix (m × o) (n × o) α) (f : α → β) :
    blockDiag (M.map f) = fun k => (blockDiag M k).map f :=
  rfl

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