English
If i1, j1, i2, j2 index basis elements and f is bilinear with f(0, b) = 0 and f(a, 0) = 0, then kroneckerMap f (single i1 j1 a) (single i2 j2 b) equals the single basis element at ((i1,i2),(j1,j2)) with value f(a,b).
Русский
При ортогональном базисе и билинейности f, если f(0, b)=0 и f(a,0)=0, то kroneckerMap f (одинарный i1 j1 a) (одинарный i2 j2 b) даёт одинарный базисный элемент с значением f(a,b).
LaTeX
$$$\operatorname{kroneckerMap} f (\text{single } i_1 j_1 a) (\text{single } i_2 j_2 b) = \text{single } {(i_1,i_2)} {(j_1,j_2)} (f(a,b))$$$
Lean4
theorem kroneckerMap_single_single [Zero α] [Zero β] [Zero γ] [DecidableEq l] [DecidableEq m] [DecidableEq n]
[DecidableEq p] (i₁ : l) (j₁ : m) (i₂ : n) (j₂ : p) (f : α → β → γ) (hf₁ : ∀ b, f 0 b = 0) (hf₂ : ∀ a, f a 0 = 0)
(a : α) (b : β) : kroneckerMap f (single i₁ j₁ a) (single i₂ j₂ b) = single (i₁, i₂) (j₁, j₂) (f a b) :=
by
ext ⟨i₁', i₂'⟩ ⟨j₁', j₂'⟩
dsimp [single]
aesop
