kroneckerMap_transpose — Mathlib

English

The Kronecker map commutes with transpose: applying kroneckerMap to A^T and B^T equals the transpose of applying kroneckerMap to A and B.

Русский

Кронекерная карта commute с транспонированием: kroneckerMap f A^T B^T = (kroneckerMap f A B)^T.

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), kroneckerMap f A^T B^T = (kroneckerMap f A B)^T$$$

Lean4

theorem kroneckerMap_transpose (f : α → β → γ) (A : Matrix l m α) (B : Matrix n p β) :
    kroneckerMap f Aᵀ Bᵀ = (kroneckerMap f A B)ᵀ :=
  ext fun _ _ => rfl

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