leftMulMatrix_apply

Mathlib.LinearAlgebra.Matrix.ToLin

URI: https://scilib.ai/kg/mathlib#Algebra.leftMulMatrix_apply

English

The leftMulMatrix map evaluated at x coincides with the matrix of left multiplication by x.

Русский

Сопоставление leftMulMatrix от образования x совпадает с матрицей левого умножения на x.

LaTeX

$$$\text{leftMulMatrix}\; b\; x = \operatorname{toMatrix}_{b b}(\mathrm{lmul}\; R\; S\; x).$$$

Lean4

theorem leftMulMatrix_apply (x : S) : leftMulMatrix b x = LinearMap.toMatrix b b (lmul R S x) :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru