quotEquivOfEq_mk — Mathlib

English

If I = J for two-sided ideals, then there is a natural ring equivalence R/I ≃+* R/J.

Русский

Если I = J для двухсторонних идеалов, существует естественное кольцевое эквивалентное отображение R/I ≃+* R/J.

LaTeX

$$$$R/I \cong+* R/J\quad\text{for } I=J.$$$$

Lean4

@[simp]
theorem quotEquivOfEq_mk (h : I = J) (x : R) : quotEquivOfEq h (Ideal.Quotient.mk I x) = Ideal.Quotient.mk J x :=
  rfl

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