map_smul₂ — Mathlib

English

Given a bilinear map f that is R-linear in the first slot and σ₁₂-linear in the second, scaling the first argument by r ∈ R corresponds to scaling the output by r.

Русский

Дано билинейное отображение f, линейное по первому аргументу и σ₁₂-линейное по второму; масштабирование первого аргумента на r соответствует масштабированию значения на r.

LaTeX

$$$ \mathrm{map\_smul\_2} (f) (r, x, y) = r \; f(x,y) $$$

Lean4

theorem map_smul₂ (f : M₂ →ₗ[R] N₂ →ₛₗ[σ₁₂] P₂) (r : R) (x y) : f (r • x) y = r • f x y :=
  (flip f y).map_smul _ _

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