如题，想要实现“矩阵直乘再乘积等于对应乘积的直乘”运算，可以通过定义
A_\[CircleTimes]B_ := KroneckerProduct[A, B];
kroneckerProductRule = (a_\[CircleTimes]b_) . (c_\[CircleTimes]d_) :> \
(a . c)\[CircleTimes](b . d);
实现。现在想将这个运算推广到多个矩阵，也即 (A \[CircleTimes] B \[CircleTimes]C) . (D \[CircleTimes] E \[CircleTimes] F) = （A . D) \[CircleTimes] (B . E) \[CircleTimes] (C . F)，尝试模式匹配后发现不成功，甚至两项矩阵都未能实现想要的结果。请问有没有大佬能解答一下。代码如下：
ClearAll["Global`*"]
mA = {{1, 2}, {3, 4}};
mC = {{1, 0}, {0, -1}};
mE = {{1, 0}, {0, 1}};
mD = {{2, 1}, {1, 0}};
A_\[CircleTimes]B_ := KroneckerProduct[A, B];
kroneckerProductRule = (a_\[CircleTimes]b_) . (c_\[CircleTimes]d_) :> \
(a . c)\[CircleTimes](b . d);
circleTimesRule =
CircleTimes[a___] . CircleTimes[b___] /;
Length[{a}] == Length[{b}] :>
CircleTimes @@ MapThread[Dot, {{a}, {b}}];
Unprotect[KroneckerProduct];
MakeBoxes[KroneckerProduct[a_, b_], StandardForm] :=
RowBox[{MakeBoxes[MatrixForm[a], StandardForm], "\[CircleTimes]",
MakeBoxes[MatrixForm[b], StandardForm]}];
Protect[KroneckerProduct];
(mA\[CircleTimes]mB) . (mE\[CircleTimes]mF)
(mA\[CircleTimes]mB) . (mE\[CircleTimes]mF) //. circleTimesRule
(mA\[CircleTimes]mB) . (mE\[CircleTimes]mF) //. kroneckerProductRule
运行结果如图：

\[CircleTimes]变KroneckerProduct可以写成规则放在最后
kroneckerProductRule = (a_\[CircleTimes]b_) . (c_\[CircleTimes]d_) :> (a . c)\[CircleTimes](b . d);
circleTimesRule = CircleTimes[a___] . CircleTimes[b___] /;Length[{a}] == Length[{b}] :>CircleTimes @@ MapThread[Dot, {{a}, {b}}];
(mA\[CircleTimes]mB) . (mE\[CircleTimes]mF)
(mA\[CircleTimes]mB\[CircleTimes]mB) . (mE\[CircleTimes]mF\[CircleTimes]mB) /. circleTimesRule
(mA\[CircleTimes]mB) . (mE\[CircleTimes]mF) /. kroneckerProductRule

尝试定义递归规则
circleTimesRule = {CircleTimes[a___] . CircleTimes[b___] /;
Length[{a}] == Length[{b}] :>
CircleTimes @@ MapThread[Dot, {{a}, {b}}],
Dot[CircleTimes[a___], CircleTimes[b___], rest___] /;
Length[{a}] == Length[{b}] :>
Dot[(CircleTimes @@ MapThread[Dot, {{a}, {b}}]), rest]};
似乎可以解决这个问题，在此记录一下

……全是计算次序问题。请思考以下两个问题：
1. 为什么
1+2 /. 2->a
不会输出1+a？
2. 观察
rule = Dot[a] :> func[a]
的输出，想想为啥会这样？
还想不明白的请阅读精品区《为什么b=a; f[a_]:=b; f[2]不输出2？——说说显式存在的重要性》那帖。