English
If S is an additive subgroup of A, then the set of m×n matrices with all entries in S forms an additive subgroup of 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\}$ является AddSubgroup подпредпосылкой в \mathrm{Mat}_{m\times n}(A).$$
Lean4
/-- A version of `Set.matrix` for `AddSubgroup`s.
Given an `AddSubgroup` `S`, `S.matrix` is the `AddSubgroup` of matrices `m`
all of whose entries `m i j` belong to `S`. -/
@[simps!]
def matrix (S : AddSubgroup A) : AddSubgroup (Matrix m n A)
where
__ := S.toAddSubmonoid.matrix
neg_mem' hm i j := AddSubgroup.neg_mem _ (hm i j)
