orderIsoMatrix

Mathlib.LinearAlgebra.Matrix.Ideal

URI: https://scilib.ai/kg/mathlib#TwoSidedIdeal.orderIsoMatrix

Lean4

/-- Two-sided ideals in $R$ are order-isomorphic with those in $Mₙ(R)$.
See also `equivMatrix`.
-/
@[simps!]
def orderIsoMatrix : TwoSidedIdeal R ≃o TwoSidedIdeal (Matrix n n R)
    where
  __ := equivMatrix
  map_rel_iff'
    {I J} := by
    simp only [equivMatrix_apply]
    constructor
    · intro le x xI
      specialize @le (of fun _ _ => x) (by simp [xI])
      simpa using le
    · intro IJ M MI i j
      exact IJ <| MI i j

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru