kroneckerBilinear — Mathlib

English

A bilinear map f gives a bilinear KroneckerMap in the composite arguments, i.e., kroneckerMap f A B is bilinear in A and B separately.

Русский

Билинейное отображение f задаёт билинейное KroneckerMap по двум аргументам отдельно.

LaTeX

$$$\text{kroneckerMap}$ является билинейным по каждому аргументу отдельно.$$

Lean4

/-- `Matrix.kronecker` as a bilinear map. -/
def kroneckerBilinear [CommSemiring R] [Semiring α] [Algebra R α] :
    Matrix l m α →ₗ[R] Matrix n p α →ₗ[R] Matrix (l × n) (m × p) α :=
  kroneckerMapBilinear (Algebra.lmul R α)

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