matrix_jacobson_le — Mathlib

English

For any ring R and ideal I, the Jacobson radical of I, when lifted to matrices, is contained in the Jacobson radical of the matrix ideal: I.jacobson.matrix n ≤ (I.matrix n).jacobson.

Русский

Для кольца R и идеала I радикал Якобсона, поднятый до матриц, содержится в радикале матричного идеала: I.jacobson.matrix n ≤ (I.matrix n).jacobson.

LaTeX

$$I.jacobson.matrix n ≤ (I.matrix n).jacobson$$

Lean4

/-- For any left ideal $I ≤ R$, we have $Mₙ(J(I)) ≤ J(Mₙ(I))$. -/
theorem matrix_jacobson_le (I : Ideal R) : I.jacobson.matrix n ≤ (I.matrix n).jacobson :=
  by
  intro M MI
  rw [matrix_eq_sum_single M]
  apply sum_mem
  intro i _
  apply sum_mem
  intro j _
  apply single_mem_jacobson_matrix I _ (MI i j)

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