polynomialQuotientEquivQuotientPolynomial_map_mk

English

The forward direction of the polynomial quotient equivalence sends mapped polynomials to their quotient images.

Русский

Прямой переход эквивалента полиномов квотирования отправляет отображения полиномов в их образы в квотированном кольце.

LaTeX

$$$I\\text{.polynomialQuotientEquivQuotientPolynomial} (f.map \\langle\\dots\\rangle) = \\text{Quotient.mk} (map C I) f$$$

Lean4

@[simp]
theorem polynomialQuotientEquivQuotientPolynomial_map_mk (I : Ideal R) (f : R[X]) :
    I.polynomialQuotientEquivQuotientPolynomial (f.map <| Quotient.mk I) = Quotient.mk (map C I : Ideal R[X]) f :=
  by
  apply (polynomialQuotientEquivQuotientPolynomial I).symm.injective
  rw [RingEquiv.symm_apply_apply, polynomialQuotientEquivQuotientPolynomial_symm_mk]

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