matrix_injective — Mathlib

English

If n is nonempty, the map I ↦ I.matrix n is injective: different ideals give different matrix ideals.

Русский

Если множество индексов непусто, отображение I ↦ I.matrix n инъективно: разные идеалы дают разные матричные идеалы.

LaTeX

$$matrix_injective : Function.Injective (matrix (R := R) n)$$

Lean4

theorem matrix_injective [Nonempty n] : Function.Injective (matrix (R := R) n) := fun I J eq ↦
  RingCon.ext fun r s ↦
    by
    have := congr_fun (DFunLike.congr_fun eq (Matrix.of fun _ _ ↦ r)) (Matrix.of fun _ _ ↦ s)
    simpa using this

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