quotQuotEquivQuotOfLE_comp_quotQuotMk

English

The composition of the LE isomorphism with the quotient map equals the direct quotient map by J: RingHom.comp (quotQuotEquivQuotOfLE h) (quotQuotMk I J) = Quotient.mk J.

Русский

Композиция изоморфизма LE с отображением квотирования равна прямому квотированию на J: композиция равна Quotient.mk J.

LaTeX

$$$\text{comp}((\quotQuotEquivQuotOfLE(h)), (\quotQuotMk I J)) = (\Ideal.Quotient.mk J)$$$

Lean4

theorem quotQuotEquivQuotOfLE_comp_quotQuotMk (h : I ≤ J) :
    RingHom.comp (↑(quotQuotEquivQuotOfLE h)) (quotQuotMk I J) = (Ideal.Quotient.mk J) :=
  by
  ext
  rfl

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