quotQuotEquivComm_mk — Mathlib

English

The mk image under quotient-quotient-comm isomorphism aligns the polynomial quotient to the coefficient ring quotient image.

Русский

Образ mk через квот- квот-комм выравнивает полином-квату к образу в кольце коэффициентов.

LaTeX

$$$\text{quotQuotEquivComm}_{{}}: (R/I)[X] / \langle f.map (I) \rangle \cong+* (R[X] /(I.map C)) / \langle f \rangle$$$

Lean4

@[simp]
theorem quotQuotEquivComm_mk (p : R[X]) :
    (Polynomial.quotQuotEquivComm I f) (Ideal.Quotient.mk _ (p.map (Ideal.Quotient.mk I))) =
      Ideal.Quotient.mk (span ({(Ideal.Quotient.mk (I.map C)) f} : Set (R[X] ⧸ (I.map C))))
        (Ideal.Quotient.mk (I.map C) p) :=
  by simp only [Polynomial.quotQuotEquivComm, quotientEquiv_mk, polynomialQuotientEquivQuotientPolynomial_map_mk]

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