kronecker_apply — Mathlib

English

The KroneckerMap is bilinear in both variables, i.e., it respects addition and scalar multiplication in each argument.

Русский

Кронекерово отображение линейно относительно обоих аргументов: по каждому аргументу сохраняется сложение и умножение на скаляр.

LaTeX

$$$\operatorname{kroneckerMap} (f) \; (A_1 \,+\ A_2) \; B = \operatorname{kroneckerMap} f A_1 B + \operatorname{kroneckerMap} f A_2 B$ и аналогично по второму аргументу.$$

Lean4

@[simp]
theorem kronecker_apply [Mul α] (A : Matrix l m α) (B : Matrix n p α) (i₁ i₂ j₁ j₂) :
    (A ⊗ₖ B) (i₁, i₂) (j₁, j₂) = A i₁ j₁ * B i₂ j₂ :=
  rfl

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