fromMatrix — Mathlib

English

PiToModule.fromMatrix maps a matrix A and a vector w to the linear combination ∑_i (A w)_i b_i in M.

Русский

PiToModule.fromMatrix переводит матрицу A и вектор w к линейной комбинации ∑_i (A w)_i b_i в M.

LaTeX

$$PiToModule.fromMatrix_R_b(A,w) = Fintype.linearCombination_R b (A *ᵥ w)$$

Lean4

/-- The composition of a matrix (as an endomorphism of `ι → R`) with the projection
`(ι → R) →ₗ[R] M`. -/
def fromMatrix [DecidableEq ι] : Matrix ι ι R →ₗ[R] (ι → R) →ₗ[R] M :=
  (LinearMap.llcomp R _ _ _ (Fintype.linearCombination R b)).comp algEquivMatrix'.symm.toLinearMap

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