leftMulMatrix_mulVec_repr — Mathlib

English

The product of the leftMulMatrix by the coordinate representation of y yields the coordinate representation of x y.

Русский

Произведение левой матрицы умножения на координаты y дает координаты произведения x y.

LaTeX

$$$\text{leftMulMatrix}\; b\; x \; *\!\!\!\!\!\!\! b\;\text{repr}\; y = b\;\text{repr}\;(x \cdot y).$$$

Lean4

theorem leftMulMatrix_mulVec_repr (x y : S) : leftMulMatrix b x *ᵥ b.repr y = b.repr (x * y) :=
  (LinearMap.mulLeft R x).toMatrix_mulVec_repr b b y

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