kroneckerMap_apply — Mathlib

English

The (i,j) entry of kroneckerMap f A B equals f(A i1 j1, B i2 j2).

Русский

Элемент (i,j) матрицы kroneckerMap f A B равен f(A(i1,j1), B(i2,j2)).

LaTeX

$$$\\forall {\\alpha} {\\beta} {\\gamma} {l} {m} {n} {p} (f : \u03b1 \u2192 \u03b2 \u2192 \u0393) (A : Matrix l m \u03b1) (B : Matrix n p \u03b2) (i j), kroneckerMap f A B i j = f (A i.1 j.1) (B i.2 j.2)$$$

Lean4

@[simp]
theorem kroneckerMap_apply (f : α → β → γ) (A : Matrix l m α) (B : Matrix n p β) (i j) :
    kroneckerMap f A B i j = f (A i.1 j.1) (B i.2 j.2) :=
  rfl

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