kroneckerMap_map_right — Mathlib

English

Applying a map g on the right argument commutes with kroneckerMap, up to composing f with g on the right.

Русский

Применение отображения g справа совместимо с kroneckerMap: kroneckerMap f A (B.map g) = kroneckerMap (λ a b, f a (g b)) A B.

LaTeX

$$$\\forall {\\alpha} {\\beta} {\\beta'} {\\gamma} {l} {m} {n} {p} (f : \\alpha \u2192 \\beta' \u2192 \\gamma) (g : \\beta \u2192 \\beta') (A : Matrix l m \\alpha) (B : Matrix n p \\beta), kroneckerMap f A (B.map g) = kroneckerMap (\\u03bb a b, f a (g b)) A B$$$

Lean4

theorem kroneckerMap_map_right (f : α → β' → γ) (g : β → β') (A : Matrix l m α) (B : Matrix n p β) :
    kroneckerMap f A (B.map g) = kroneckerMap (fun a b => f a (g b)) A B :=
  ext fun _ _ => rfl

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