coe_equivMatrix_symm_apply — Mathlib

English

For any R, i, j, and a two-sided ideal I in M_n(R), the inverse-equivalence image satisfies: equivMatrix.symm I = { N_{ij} | N ∈ I }.

Русский

Для любого кольца R, индексов i, j и двусторонней идеал I в M_n(R) обратное по эквивалентности совпадает с множеством { N_{ij} | N ∈ I }.

LaTeX

$$$$ \\mathrm{equivMatrix}.\\mathrm{symm}(I) = \\{ N_{ij} \\mid N \\in I \\}. $$$$

Lean4

theorem coe_equivMatrix_symm_apply (I : TwoSidedIdeal (Matrix n n R)) (i j : n) :
    equivMatrix.symm I = {N i j | N ∈ I} := by
  ext r
  constructor
  · intro h
    exact ⟨single i j r, by simpa using h i j, by simp⟩
  · rintro ⟨n, hn, rfl⟩
    rw [SetLike.mem_coe, mem_iff, equivMatrix_symm_apply_ringCon, RingCon.coe_ofMatrix_eq_relationMap i j]
    exact ⟨n, 0, (I.mem_iff n).mp hn, rfl, rfl⟩

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