kronecker — Mathlib

English

The Kronecker product is the special case kroneckerMap with multiplication, i.e., A ⊗ B = kroneckerMap (· × ·) A B.

Русский

Кронекерово произведение — это частный случай kroneckerMap, где операция — умножение: A ⊗ B = kroneckerMap (×) A B.

LaTeX

$$$\mathrm{kronecker} = \mathrm{kroneckerMap} (\cdot \cdot)$$$

Lean4

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

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