quotEquivQuotMap_symm_apply_mk — Mathlib

English

A further symmetric application shows the equality of the image under the inverse map when applied to mk (I) of a polynomial g.

Русский

Ещё одно симметричное применение показывает равенство образа под обратной картой к mk(I) g.

LaTeX

$$quotEquivQuotMap_symm_apply_mk: = (AdjoinRoot.quotEquivQuotMap f I).symm (Ideal.Quotient.mk _ (Polynomial.map (Ideal.Quotient.mk I) g)) = Ideal.Quotient.mk (I.map (of f)) (AdjoinRoot.mk f g)$$

Lean4

theorem quotEquivQuotMap_symm_apply_mk (f g : R[X]) (I : Ideal R) :
    (AdjoinRoot.quotEquivQuotMap f I).symm (Ideal.Quotient.mk _ (Polynomial.map (Ideal.Quotient.mk I) g)) =
      Ideal.Quotient.mk (Ideal.map (of f) I) (AdjoinRoot.mk f g) :=
  by rw [AdjoinRoot.quotEquivQuotMap_symm_apply, AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_symm_mk_mk]

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