English
The left multiplication by a fixed submodule element distributes over the finsupp-sum in the canonical way.
Русский
Левостороннее умножение на фиксированный элемент подмодуля распределяется по сумме finsupp обычным образом.
LaTeX
$$$mulLeftMap N m n = Finsupp.sum n (\lambda i, \lambda x, (m i).1 * x.1)$$$
Lean4
/-- If `M` and `N` are submodules of an `R`-algebra `S`, `m : ι → M` is a family of elements, then
there is an `R`-linear map from `ι →₀ N` to `S` which maps `{ n_i }` to the sum of `m_i * n_i`.
This is used in the definition of linearly disjointness. -/
def mulLeftMap {M : Submodule R S} (N : Submodule R S) {ι : Type*} (m : ι → M) : (ι →₀ N) →ₗ[R] S :=
Finsupp.lsum R fun i ↦ (m i).1 • N.subtype
