quotEquivOfEq — Mathlib

English

If I and J are two-sided ideals with I = J in a ring R, then R/I is ring-isomorphic to R/J.

Русский

Пусть I и J — двусторонние идеалы кольца R и I = J. Тогда R/I и R/J изоморфны как кольца.

LaTeX

$$$$R/I \cong R/J \quad\text{whenever}\quad I = J,$$$$

Lean4

/-- Quotienting by equal ideals gives equivalent rings.

See also `Submodule.quotEquivOfEq` and `Ideal.quotientEquivAlgOfEq`.
-/
def quotEquivOfEq (h : I = J) : R ⧸ I ≃+* R ⧸ J :=
  { Submodule.quotEquivOfEq I J h with
    map_mul' := by
      rintro ⟨x⟩ ⟨y⟩
      rfl }

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