toMatrixAux — Mathlib

English

The product of the matrix representing the basis b with the Pi-basisFun matrix A yields a matrix whose (i,j) entry is b.repr(A.col j) i.

Русский

Произведение матрицы базы b на A, записанной в виде Pi-basisFun, даёт матрицу с i,j-ным элементом b.repr(A.col j) i.

LaTeX

$$$ b.toMatrix (Pi.basisFun R ι) \cdot A = \mathrm{of} (i,j) \mapsto b.repr (A.col j) i $$$

Lean4

/-- The linear map from bilinear forms to `Matrix n n R` given an `n`-indexed basis.

This is an auxiliary definition for the equivalence `Matrix.toBilin'`. -/
def toMatrixAux (b : n → M₁) : BilinForm R₁ M₁ →ₗ[R₁] Matrix n n R₁ :=
  LinearMap.toMatrix₂Aux R₁ b b

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