toMatrix_smul — Mathlib

English

Scaling the basis by a scalar induces a corresponding left action on the matrix: (g • e).toMatrix v = e.toMatrix (g^{-1} • v).

Русский

Умножение базиса на скаляр g слева вызывает обратное действие на матрицу: (g • e).toMatrix v = e.toMatrix (g^{-1} • v).

LaTeX

$$toMatrix_smul_left (g) : (g • e).toMatrix v = e.toMatrix (g^{-1} • v)$$

Lean4

theorem toMatrix_smul {R₁ S : Type*} [CommSemiring R₁] [Semiring S] [Algebra R₁ S] [Fintype ι] [DecidableEq ι] (x : S)
    (b : Basis ι R₁ S) (w : ι → S) : (b.toMatrix (x • w)) = (Algebra.leftMulMatrix b x) * (b.toMatrix w) :=
  by
  ext
  rw [Basis.toMatrix_apply, Pi.smul_apply, smul_eq_mul, ← Algebra.leftMulMatrix_mulVec_repr]
  rfl

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