leftMulMatrix_eq_repr_mul — Mathlib

English

The (i,j) entry of leftMulMatrix b x equals the i-th coordinate of x times the j-th basis vector in b.

Русский

(i,j) элементы leftMulMatrix b x равны i‑й координате x·b_j в базисе b.

LaTeX

$$$\text{leftMulMatrix}\; b\; x\; i j = b.repr(x \cdot b_j)_i.$$$

Lean4

theorem leftMulMatrix_eq_repr_mul (x : S) (i j) : leftMulMatrix b x i j = b.repr (x * b j) i := by
  -- This is defeq to just `toMatrix_lmul' b x i j`,
    -- but the unfolding goes a lot faster with this explicit `rw`.
  rw [leftMulMatrix_apply, toMatrix_lmul' b x i j]

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