polynomialQuotientEquivQuotientPolynomial_symm_mk

English

The symm map of polynomial quotient has a compatibility with the mk-map of polynomials.

Русский

Сопряжённое отображение квотирования совместимо с отображением mk полиномов.

LaTeX

$$$\\text{polynomialQuotientEquivQuotientPolynomial_symm_mk}$$$

Lean4

@[simp]
theorem polynomialQuotientEquivQuotientPolynomial_symm_mk (I : Ideal R) (f : R[X]) :
    I.polynomialQuotientEquivQuotientPolynomial.symm (Quotient.mk _ f) = f.map (Quotient.mk I) := by
  rw [polynomialQuotientEquivQuotientPolynomial, RingEquiv.symm_mk, RingEquiv.coe_mk, Equiv.coe_fn_mk, Quotient.lift_mk,
    coe_eval₂RingHom, eval₂_eq_eval_map, ← Polynomial.map_map, ← eval₂_eq_eval_map, Polynomial.eval₂_C_X]

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