matrix_jacobson_bot — Mathlib

English

Equality of Jacobson radicals of bottom ideals respects the matrix construction: (⊥ : TwoSidedIdeal R).jacobson.matrix n = (⊥ : TwoSidedIdeal (Matrix n n R)).jacobson.

Русский

Равенство радикала Якобсона для нижних идеалов сохраняется при построении матриц: (⊥).jacobson.matrix n = (⊥)matrixn(R).jacobson.

LaTeX

$$$$ (\\perp)^{\\mathrm{jacobson}}_n = (\\perp^{\\mathrm{jacobson}})_{\\mathrm{matrix}}^{(n)}. $$$$

Lean4

theorem matrix_jacobson_bot : (⊥ : TwoSidedIdeal R).jacobson.matrix n = (⊥ : TwoSidedIdeal (Matrix n n R)).jacobson :=
  matrix_bot n (R := R) ▸ (jacobson_matrix _).symm

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