English
The leftMulMatrix with a tower of bases equals the composite of leftMulMatrix for each base, respecting tower structure.
Русский
Левое умножение через башню базисов эквивалентно композиции левых матриц базисов по башне.
LaTeX
$$$\text{leftMulMatrix}(b.smulTower c)\; x = \text{leftMulMatrix}(b) \bigl(\text{leftMulMatrix}(c)\; x\bigr).$$$
Lean4
@[simp]
theorem smul_leftMulMatrix {G} [Group G] [DistribMulAction G S] [SMulCommClass G R S] [SMulCommClass G S S] (g : G)
(x) : leftMulMatrix (g • b) x = leftMulMatrix b x := by
ext
simp_rw [leftMulMatrix_apply, LinearMap.toMatrix_apply, coe_lmul_eq_mul, LinearMap.mul_apply', Basis.repr_smul,
Basis.smul_apply, LinearEquiv.trans_apply, DistribMulAction.toLinearEquiv_symm_apply, mul_smul_comm, inv_smul_smul]
