English
For any ideal I in a ring R, the left ideal of matrices with entries from I forms an ideal inside the matrix ring: each matrix with entries in I behaves compatibly with matrix addition and multiplication on the left.
Русский
Для любого идеала I в кольце R, левый идеал матриц с элементами из I образует идеал внутри кольца матриц: каждая матрица с элементами из I совместима с матричным сложением и умножением слева.
LaTeX
$$def matrix (I : Ideal R) : Ideal (Matrix n n R) where __ := I.toAddSubmonoid.matrix$$
Lean4
/-- The left ideal of matrices with entries in `I ≤ R`. -/
def matrix (I : Ideal R) : Ideal (Matrix n n R)
where
__ := I.toAddSubmonoid.matrix
smul_mem' M N
hN := by
intro i j
rw [smul_eq_mul, mul_apply]
apply sum_mem
intro k _
apply I.mul_mem_left _ (hN k j)
