quotMapOfEquivQuotMapCMapSpanMk_symm_mk

English

Symmetric image under the inverse of quotMapOfEquivQuotMapCMapSpanMk sends mk f p to mk f p in the original quotient.

Русский

Образ при обратном отображении quotMapOfEquivQuotMapCMapSpanMk отправляет mk f p в исходный элемент.

LaTeX

$$$(quotMapOfEquivQuotMapCMapSpanMk I f).symm\; (Ideal.Quotient.mk (span { f }) (mk f p)) = Ideal.Quotient.mk (I.map (of f)) (mk f p)$$$

Lean4

theorem quotMapOfEquivQuotMapCMapSpanMk_symm_mk (x : AdjoinRoot f) :
    (quotMapOfEquivQuotMapCMapSpanMk I f).symm
        (Ideal.Quotient.mk ((I.map (C : R →+* R[X])).map (Ideal.Quotient.mk (span { f }))) x) =
      Ideal.Quotient.mk (I.map (of f)) x :=
  by
  rw [quotMapOfEquivQuotMapCMapSpanMk, Ideal.quotEquivOfEq_symm]
  exact Ideal.quotEquivOfEq_mk _ _

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