smulTower_leftMulMatrix — Mathlib

English

Equality between the tower-based left multiplication and the product of base left multiplications.

Русский

Эквивалентность между башенным левым умножением и произведением левых умножений базисов.

LaTeX

$$$\text{smulTower_leftMulMatrix_eq}(b,c,x,i,j) :\; \cdot$$$

Lean4

theorem smulTower_leftMulMatrix (x) (ik jk) :
    leftMulMatrix (b.smulTower c) x ik jk = leftMulMatrix b (leftMulMatrix c x ik.2 jk.2) ik.1 jk.1 := by
  simp only [leftMulMatrix_apply, LinearMap.toMatrix_apply, mul_comm, Basis.smulTower_apply, Basis.smulTower_repr,
    Finsupp.smul_apply, id.smul_eq_mul, LinearEquiv.map_smul, mul_smul_comm, coe_lmul_eq_mul, LinearMap.mul_apply']

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