Theorems · Definition · ring theory

TwoSidedIdeal.equivMatrix

{R : Type u_1} →
  {n : Type u_2} →
    [inst : NonAssocRing R] →
      [inst_1 : Fintype n] → [Nonempty n] → [DecidableEq n] → TwoSidedIdeal R ≃ TwoSidedIdeal (Matrix n n R)

Two-sided ideals in $R$ correspond bijectively to those in $Mₙ(R)$. Given an ideal $I ≤ R$, we send it to $Mₙ(I)$. Given an ideal $J ≤ Mₙ(R)$, we send it to $\{Nᵢⱼ ∣ ∃ N ∈ J\}$.

Defined in

Mathlib.LinearAlgebra.Matrix.Ideal

Cited by

4 results in Mathlib

Foundations

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

Assumes

NonAssocRingFintypeNonemptyDecidableEq