kroneckerMap_smul_right — Mathlib

English

If f is linear in the second argument, i.e., f(a, r·b) = r·f(a, b), then kroneckerMap f A (r · B) = r · kroneckerMap f A B.

Русский

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

LaTeX

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

Lean4

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

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