kroneckerMap_map_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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