blockDiagonal'_add — Mathlib

English

BlockDiagonal' preserves addition: blockDiagonal'(M+N) = blockDiagonal'M + blockDiagonal'N.

Русский

BlockDiagonal' сохраняет сложение: blockDiagonal'(M+N) = blockDiagonal'M + blockDiagonal'N.

LaTeX

$$$ \\mathrm{blockDiagonal}'(M + N) = \\mathrm{blockDiagonal}' M + \\mathrm{blockDiagonal}' N $$$

Lean4

@[simp]
theorem blockDiagonal'_add [AddZeroClass α] (M N : ∀ i, Matrix (m' i) (n' i) α) :
    blockDiagonal' (M + N) = blockDiagonal' M + blockDiagonal' N :=
  by
  ext
  simp only [blockDiagonal'_apply, Pi.add_apply, add_apply]
  split_ifs <;> simp

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