matrix — Mathlib

English

If I is a two-sided ideal of R, then the set of all n×n matrices with every entry belonging to I forms a two-sided ideal in M_n(R).

Русский

Если I — двусторонняя идеал R, то множество всех матриц размером n×n, чьи все элементы принадлежат I, образует двустороннюю идеал в M_n(R).

LaTeX

$$$$ I^{\\mathrm{matrix}}_n := \\{ A \\in M_n(R) : \\forall p,q,\\; A_{pq} \\in I \\} \\text{ is a two-sided ideal of } M_n(R). $$$$

Lean4

/-- The two-sided ideal of matrices with entries in `I ≤ R`. -/
@[simps]
def matrix (I : TwoSidedIdeal R) : TwoSidedIdeal (Matrix n n R) where ringCon := I.ringCon.matrix n

Похожие утверждения