toFunBilinear_apply — Mathlib

English

The bilinear mapping underlying the action of A on matrices is given by a · M mapped via the algebra map, i.e., toFunBilinear(a, M) = a · M.map(algebraMap_R^A).

Русский

Две линейные переменные образуют билинейную связку: действие A на матрицы задано как a · M, приводимое через отображение алгебраической карты.

LaTeX

$$$ toFunBilinear(n,R,A)(a,M) = a \cdot M^{\#}, \text{ with } M^{\#}_{ij} = (algebraMap_R^A)(M_{ij}) $$$

Lean4

@[simp]
theorem toFunBilinear_apply (a : A) (m : Matrix n n R) : toFunBilinear n R A a m = a • m.map (algebraMap R A) :=
  rfl

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