blockDiagonal'_transpose — Mathlib

English

BlockDiagonal' commutes with transpose across indices.

Русский

BlockDiagonal' обращается с транспонированием по индексу.

LaTeX

$$$ (blockDiagonal' M)^{T} = blockDiagonal' (M)^{T} $$$

Lean4

@[simp]
theorem blockDiagonal'_transpose (M : ∀ i, Matrix (m' i) (n' i) α) :
    (blockDiagonal' M)ᵀ = blockDiagonal' fun k => (M k)ᵀ :=
  by
  ext ⟨ii, ix⟩ ⟨ji, jx⟩
  simp only [transpose_apply, blockDiagonal'_apply]
  split_ifs <;> grind

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