blockDiag'_smul — Mathlib

English

Let R be a ring acting on α via a scalar multiplication. For any x ∈ R and any matrix M with entries in α, blockDiag'(x • M) = x • blockDiag'(M).

Русский

Пусть R действует на α скалярно. Для любого x ∈ R и любой матрицы M с элементами из α выполняется blockDiag'(x • M) = x • blockDiag'(M).

LaTeX

$$$blockDiag'(x \\cdot M) = x \\cdot blockDiag'(M)$$$

Lean4

@[simp]
theorem blockDiag'_smul {R : Type*} [SMul R α] (x : R) (M : Matrix (Σ i, m' i) (Σ i, n' i) α) :
    blockDiag' (x • M) = x • blockDiag' M :=
  rfl

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