blockDiagonal'_map — Mathlib

English

Transposing blockDiagonal' equals blockDiagonal' of transposed M.

Русский

Транспонирование blockDiagonal' эквивалентно блочной диагонали транспонированного M.

LaTeX

$$$ (blockDiagonal' M)^T = blockDiagonal' (k \mapsto M_k)^T $$$

Lean4

theorem blockDiagonal'_map (M : ∀ i, Matrix (m' i) (n' i) α) (f : α → β) (hf : f 0 = 0) :
    (blockDiagonal' M).map f = blockDiagonal' fun k => (M k).map f :=
  by
  ext
  simp only [map_apply, blockDiagonal'_apply]
  rw [apply_dite f, hf]

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