English
If S is a Submodule of a module M over a ring R, then the set of m×n matrices with entries in S forms a Submodule of the matrix module M^{m×n}.
Русский
Если S — подмодуль M над кольцом R, то множество матриц размерности m×n со всеми элементами из S образует подмодуль матричного пространства M^{m×n}.
LaTeX
$$$\{M \in \mathrm{Mat}_{m\times n}(M) \;|\; \forall i,j:\ M_{ij} \in S\}$ является Submodule матричного пространства \mathrm{Mat}_{m\times n}(M).$$
Lean4
/-- A version of `Set.matrix` for `Submodule`s.
Given a `Submodule` `S`, `S.matrix` is the `Submodule` of matrices `m`
all of whose entries `m i j` belong to `S`. -/
@[simps!]
def matrix (S : Submodule R M) : Submodule R (Matrix m n M)
where
__ := S.toAddSubmonoid.matrix
smul_mem' _ _ hm i j := Submodule.smul_mem _ _ (hm i j)
