kroneckerTMul — Mathlib

English

The Kronecker tensor product is defined as a shorthand: kroneckerTMul := kroneckerMap (· ⊗ₜ ·).

Русский

Кронекеров тензорный продукт — это определение-заметка: kroneckerTMul := kroneckerMap (⊗ₜ).

LaTeX

$$$ \text{kroneckerTMul} \colon M_{l,m}(\alpha) \to M_{n,p}(\beta) \to M_{l \times n, m \times p}(\alpha \otimes_R \beta) \\ \text{defined as } \text{kroneckerTMul} = \text{kroneckerMap}(\cdot \otimes_\mathrm{t} \cdot)$$$

Lean4

/-- The Kronecker tensor product. This is just a shorthand for `kroneckerMap (⊗ₜ)`.
Prefer the notation `⊗ₖₜ` rather than this definition. -/
@[simp]
def kroneckerTMul : Matrix l m α → Matrix n p β → Matrix (l × n) (m × p) (α ⊗[R] β) :=
  kroneckerMap (· ⊗ₜ ·)

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