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