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