English
The matrix of the product map φ1.prod φ2 with respect to the product basis is the block matrix with φ1 and φ2 on the diagonal blocks and zeros elsewhere.
Русский
Матрица отображения φ1.prod φ2 относительно базиса произведения есть блочная матрица с φ1 и φ2 на диагональных блоках и нулями в остальных местах.
LaTeX
$$$\operatorname{toMatrix} (v_1.\mathrm{prod} v_2) (v_1.\mathrm{prod} v_2)(\varphi_1.\mathrm{prodMap} \varphi_2) = \mathrm{Matrix.fromBlocks}(\operatorname{toMatrix}_{v_1 v_1}(\varphi_1), 0, 0, \operatorname{toMatrix}_{v_2 v_2}(\varphi_2)).$$$
Lean4
@[simp]
theorem toMatrix_distrib_mul_action_toLinearMap (x : R) :
LinearMap.toMatrix v₁ v₁ (DistribMulAction.toLinearMap R M₁ x) = Matrix.diagonal fun _ ↦ x :=
by
ext
rw [LinearMap.toMatrix_apply, DistribMulAction.toLinearMap_apply, LinearEquiv.map_smul, Basis.repr_self,
Finsupp.smul_single_one, Finsupp.single_eq_pi_single, Matrix.diagonal_apply, Pi.single_apply]
