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