Theorems · Theorem · ring theory

TwoSidedIdeal.jacobson_matrix

∀ {R : Type u_1} [inst : Ring R] {n : Type u_2} [inst_1 : Fintype n] [inst_2 : DecidableEq n] (I : TwoSidedIdeal R),
  (TwoSidedIdeal.matrix n I).jacobson = TwoSidedIdeal.matrix n I.jacobson

For any two-sided ideal $I ≤ R$, we have $J(Mₙ(I)) = Mₙ(J(I))$.

Defined in

Mathlib.LinearAlgebra.Matrix.Ideal

Cited by

1 results in Mathlib

Foundations

Depth 87 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingFintypeDecidableEq