English
The matrix of a product map on a direct product decomposes as a block diagonal matrix composed of the blocks corresponding to each factor.
Русский
Матрица произведения отображений на прямом сумме распадается на блочную диагональ, где каждое блок‑подматрица соответствует одному фактору.
LaTeX
$$$\operatorname{toMatrix}_{v_1\!\!\!\!\!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
theorem toLin_finTwoProd (a b c d : R) :
Matrix.toLin (Basis.finTwoProd R) (Basis.finTwoProd R) !![a, b; c, d] =
(a • LinearMap.fst R R R + b • LinearMap.snd R R R).prod (c • LinearMap.fst R R R + d • LinearMap.snd R R R) :=
LinearMap.ext <| Matrix.toLin_finTwoProd_apply _ _ _ _
