quotQuotEquivQuotOfLE_symm_comp_mk

English

The symmetrized form of quotQuotEquivQuotOfLE, composed with quotQuotMk I J, equals the mk J map: (quotQuotEquivQuotOfLE h)^{-1} ∘ (Ideal.Quotient.mk J) = quotQuotMk I J.

Русский

Симметричная форма quotQuotEquivQuotOfLE, составленная с quotQuotMk I J, равна mk I J: ( (quotQuotEquivQuotOfLE h)^{-1} ) ∘ (Ideal.Quotient.mk J) = quotQuotMk I J.

LaTeX

$$$(\quotQuotEquivQuotOfLE(h))^{-1} \circ (\Ideal.Quotient.mk J) = \quotQuotMk I J$$$

Lean4

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

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