quotQuotEquivQuotOfLE — Mathlib

English

If I ≤ J are ideals of a commutative ring R, there is a canonical ring isomorphism between (R/I) modulo the image of J in R/I and R/J; this is the Third Isomorphism Theorem for rings.

Русский

Если I ⊆ J — идеалы кольца R, существует каноническое кольцевое изоморфизм между (R/I) ⧸ (J.map mk I) и R/J; это Теорема третьего изomорфизма для колец.

LaTeX

$$$((R/I) / (J \text{ mapped by } \text{mk } I)) \cong R/J$$$

Lean4

/-- **The Third Isomorphism theorem** for rings. See `quotQuotEquivQuotSup` for a version
    that does not assume an inclusion of ideals. -/
def quotQuotEquivQuotOfLE (h : I ≤ J) : (R ⧸ I) ⧸ J.map (Ideal.Quotient.mk I) ≃+* R ⧸ J :=
  (quotQuotEquivQuotSup I J).trans (Ideal.quotEquivOfEq <| sup_eq_right.mpr h)

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