toMatrix_prodMap — Mathlib

English

The matrix representing the action of a scalar x on M1 is the diagonal matrix with x on every diagonal entry.

Русский

Матрица действия скаляра x на M1 по базису является диагональной матрицей с x на диагонали.

LaTeX

$$$\operatorname{toMatrix}_{v_1 v_1}(\DistribMulAction.toLinearMap\; R\; M_1\; x) = \operatorname{diag}(x).$$$

Lean4

theorem toMatrix_prodMap [DecidableEq m] [DecidableEq (n ⊕ m)] (φ₁ : Module.End R M₁) (φ₂ : Module.End R M₂) :
    toMatrix (v₁.prod v₂) (v₁.prod v₂) (φ₁.prodMap φ₂) =
      Matrix.fromBlocks (toMatrix v₁ v₁ φ₁) 0 0 (toMatrix v₂ v₂ φ₂) :=
  by ext (i | i) (j | j) <;> simp [toMatrix]

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