mulVecBilin — Mathlib

English

The map M ↦ (n→A) ↦ (m→A) given by M ↦ M *ᵥ x is bilinear in M and x.

Русский

Отображение M ↦ (n→A) ↦ (m→A), заданное M ↦ M *ᵥ x, билинейно по M и x.

LaTeX

$$MulVecBilin : Matrix m n A →ₗ[R] (n → A) →ₗ[S] (m → A)$$

Lean4

/-- `Matrix.mulVec` as a bilinear map.

When `A` is non-commutative, this can be instantiated as `mulVecBilin A Aᵐᵒᵖ` -/
def mulVecBilin [Fintype n] : Matrix m n A →ₗ[R] (n → A) →ₗ[S] (m → A)
    where
  toFun
    M :=
    { toFun x := M *ᵥ x
      map_add' _ _ := mulVec_add _ _ _
      map_smul' _ _ := mulVec_smul _ _ _ }
  map_add' _ _ := LinearMap.ext fun _ => add_mulVec _ _ _
  map_smul' _ _ := LinearMap.ext fun _ => smul_mulVec _ _ _

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