blockDiagonal'_smul — Mathlib

English

BlockDiagonal' is injective; equality of blockDiagonal' M and blockDiagonal' N implies M = N.

Русский

Блочно-диагональная инъекция: равенство blockDiagonal' M и blockDiagonal' N влечёт M = N.

LaTeX

$$$ \\mathrm{blockDiagonal}' M = \\mathrm{blockDiagonal}' N \\iff M = N $$$

Lean4

@[simp]
theorem blockDiagonal'_smul {R : Type*} [Zero α] [SMulZeroClass R α] (x : R) (M : ∀ i, Matrix (m' i) (n' i) α) :
    blockDiagonal' (x • M) = x • blockDiagonal' M := by
  ext
  simp only [blockDiagonal'_apply, Pi.smul_apply, smul_apply]
  split_ifs <;> simp

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