toMatrix_lmul_eq — Mathlib

English

When restricting scalars from A to R, the matrix of the restricted map corresponds to applying leftMulMatrix after mapping through the scalar restriction.

Русский

При ограничении скаляров отображение сохраняется в матрицу через leftMulMatrix и соответствующее отображение на скалярах.

LaTeX

$$$\operatorname{toMatrix}(\text{bA.smulTower' bM}) (\text{bA.smulTower' bM}) (\operatorname{restrictScalars}\; R\; f) = (\operatorname{toMatrix}\; bM\; bM\; f).map(\operatorname{leftMulMatrix}\; bA)\,.$$$

Lean4

@[simp]
theorem toMatrix_lmul_eq (x : S) : LinearMap.toMatrix b b (LinearMap.mulLeft R x) = leftMulMatrix b x :=
  rfl

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