kroneckerTMulBilinear_apply — Mathlib

English

Evaluating the Kronecker bilinear map on A and B yields the canonical Kronecker product A ⊗_R B.

Русский

Пусть применяют билинейное отображение Кронекера к A и B; результатом является каноническое кронекерово произведение A ⊗_R B.

LaTeX

$$$kroneckerTMulBilinear\, R\, S\, A\, B = A \otimes_{\!R} B$$$

Lean4

@[simp]
theorem kroneckerTMulBilinear_apply [Semiring S] [Module S α] [SMulCommClass R S α] (A : Matrix l m α)
    (B : Matrix n p β) : kroneckerTMulBilinear R S A B = A ⊗ₖₜ[R] B :=
  rfl

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