English
The family smulRightₗ is bilinear in its two arguments: f, x behave bilinearly with respect to addition and scalar multiplication.
Русский
Семейство smulRightₗ двуполсло линейно по двум аргументам: f и x ведут себя билинейно по сложению и умножению на скаляры.
LaTeX
$$smulRightₗ : (M₂ →ₗ[R] R) →ₗ[R] M →ₗ[R] M₂ →ₗ[R] M with bilinearity in f and x$$
Lean4
/-- The family of linear maps `M₂ → M` parameterised by `f ∈ M₂ → R`, `x ∈ M`, is linear in `f`, `x`.
-/
def smulRightₗ : (M₂ →ₗ[R] R) →ₗ[R] M →ₗ[R] M₂ →ₗ[R] M
where
toFun
f :=
{ toFun := LinearMap.smulRight f
map_add' := fun m m' => by
ext
apply smul_add
map_smul' := fun c m => by
ext
apply smul_comm }
map_add' f
f' := by
ext
apply add_smul
map_smul' c
f := by
ext
apply mul_smul
