kroneckerMap_smul_left — Mathlib

English

If f is linear in the scalar action on the first argument, i.e., f(r·a, b) = r·f(a, b), then kroneckerMap f (r • A) B = r • kroneckerMap f A B.

Русский

Если f линейно по отношению к действию на первый аргумент: f(r·a, b) = r·f(a, b), тогда kroneckerMap f (r • A) B = r · kroneckerMap f A B.

LaTeX

$$$\operatorname{kroneckerMap} f (r \cdot A) B = r \cdot \operatorname{kroneckerMap} f A B$$$

Lean4

theorem kroneckerMap_smul_left [SMul R α] [SMul R γ] (f : α → β → γ) (r : R) (hf : ∀ a b, f (r • a) b = r • f a b)
    (A : Matrix l m α) (B : Matrix n p β) : kroneckerMap f (r • A) B = r • kroneckerMap f A B :=
  ext fun _ _ => hf _ _

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