blockDiag'_transpose — Mathlib

English

There is a ring homomorphism structure on blockDiagonal', turning families of block matrices into a single block matrix with the same multiplication.

Русский

Существует структура кольцевого однородного отображения на blockDiagonal', переводящая семейство блочных матриц в одну блочную матрицу с сохранением умножения.

LaTeX

$$$ \\mathrm{blockDiagonal' RingHom} : (\\forall i, Matrix (m' i)(m' i) \\alpha) \\to* Matrix (\\Sigma i, m' i) (\\Sigma i, m' i) \\alpha $$$

Lean4

@[simp]
theorem blockDiag'_transpose (M : Matrix (Σ i, m' i) (Σ i, n' i) α) (k : o) : blockDiag' Mᵀ k = (blockDiag' M k)ᵀ :=
  ext fun _ _ => rfl

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