basisRepr_apply — Mathlib

English

Scaling a quadratic map by a scalar scales its matrix representation by the same scalar in the matrix sense.

Русский

Умножение квадратичной карты на скаляр масштабирует её матричное представление тем же скаляром.

LaTeX

$$(a • Q).toMatrix' = a • Q.toMatrix'$$

Lean4

@[simp]
theorem basisRepr_apply [Fintype ι] {v : Basis ι R M} (Q : QuadraticMap R M N) (w : ι → R) :
    Q.basisRepr v w = Q (∑ i : ι, w i • v i) :=
  by
  rw [← v.equivFun_symm_apply]
  rfl

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