English
If S is an additive submonoid of A, then the set of m×n matrices with all entries in S forms an additive submonoid of the matrix monoid M_{m×n}(A).
Русский
Пусть S является аддитивной подмоноидой A; тогда множество матриц размером m×n все элементы которых принадлежат S образует аддитивную подмножество подножество матриц M_{m×n}(A).
LaTeX
$$$\{M \in \mathrm{Mat}_{m\times n}(A) \;|\; \forall i,j:\ M_{ij} \in S\}$ является аддитивной подпредпосылкой (AddSubmonoid) в \mathrm{Mat}_{m\times n}(A).$$
Lean4
/-- A version of `Set.matrix` for `AddSubmonoid`s.
Given an `AddSubmonoid` `S`, `S.matrix` is the `AddSubmonoid` of matrices `m`
all of whose entries `m i j` belong to `S`. -/
@[simps]
def matrix (S : AddSubmonoid A) : AddSubmonoid (Matrix m n A)
where
carrier := Set.matrix S
add_mem' hm hn i j := add_mem (hm i j) (hn i j)
zero_mem' _ _ := zero_mem _
