fromBlocks_diagonal — Mathlib

English

From blocks with diagonals on both sides yields a diagonal matrix whose diagonal is Sum.elim of the two diagonal lists.

Русский

Из блочной диагонали диагональные списки складываются функцией Sum.elim: fromBlocks (diagonal d₁) 0 0 (diagonal d₂) = diagonal (Sum.elim d₁ d₂).

LaTeX

$$$ \\text{fromBlocks }(\\text{diagonal } d_1) \\ 0 \\ 0 \\ (\\text{diagonal } d_2) = \\text{diagonal } (\\text{Sum.elim } d_1 d_2) $$$

Lean4

@[simp]
theorem fromBlocks_diagonal (d₁ : l → α) (d₂ : m → α) :
    fromBlocks (diagonal d₁) 0 0 (diagonal d₂) = diagonal (Sum.elim d₁ d₂) :=
  by
  ext i j
  rcases i with ⟨⟩ <;> rcases j with ⟨⟩ <;> simp [diagonal]

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