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