toMatrix_lmul' — Mathlib

English

For algebra L, the matrix of left multiplication by x is given by the entries b.repr(x·b_j) i, i.e. the matrix of the map y ↦ x·y.

Русский

Матрица левого умножения на x по базису b имеет i,j‑й элемент равный координате x·b_j вдоль b_i.

LaTeX

$$$\operatorname{toMatrix}_{b b}(\mathrm{lmul}\; R\; S\; x)_{i j} = b.repr(x \cdot b_j)_i.$$$

Lean4

theorem toMatrix_lmul' (x : S) (i j) : LinearMap.toMatrix b b (lmul R S x) i j = b.repr (x * b j) i := by
  simp only [LinearMap.toMatrix_apply', coe_lmul_eq_mul, LinearMap.mul_apply']

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