English
The evaluation of mulLeftMap on a finsupp n by a vector corresponds to the pointwise product of the left submodule component with the right argument.
Русский
Оценка mulLeftMap на finsupp n на вектор дает попарное произведение компонента слева со значением справа.
LaTeX
$$mulLeftMap N m n = Finsupp.sum n (\i t, (m i).1 * t.1)$$
Lean4
/-- If `M` and `N` are submodules of an `R`-algebra `S`, `n : ι → N` is a family of elements, then
there is an `R`-linear map from `ι →₀ M` to `S` which maps `{ m_i }` to the sum of `m_i * n_i`.
This is used in the definition of linearly disjointness. -/
def mulRightMap (M : Submodule R S) {N : Submodule R S} {ι : Type*} (n : ι → N) : (ι →₀ M) →ₗ[R] S :=
Finsupp.lsum R fun i ↦ MulOpposite.op (n i).1 • M.subtype
