English
The symmetry of the quotAdjoinRootEquivQuotPolynomialQuot when applied to mk f p yields mk of p in the base quotient.
Русский
Симметрия quotAdjoinRootEquivQuotPolynomialQuot, применённая к mk f p, даёт mk p в базовой квоте.
LaTeX
$$quotAdjoinRootEquivQuotPolynomialQuot_symm_mk_mk: = (quotAdjoinRootEquivQuotPolynomialQuot I f).symm (Ideal.Quotient.mk (span ({f.map (Ideal.Quotient.mk I)} : Set (R ⧸ I)[X])) (p.map (Ideal.Quotient.mk I))) = Ideal.Quotient.mk (I.map (of f)) (mk f p)$$
Lean4
@[simp]
theorem quotAdjoinRootEquivQuotPolynomialQuot_symm_mk_mk (p : R[X]) :
(quotAdjoinRootEquivQuotPolynomialQuot I f).symm
(Ideal.Quotient.mk (span ({f.map (Ideal.Quotient.mk I)} : Set (R ⧸ I)[X])) (p.map (Ideal.Quotient.mk I))) =
Ideal.Quotient.mk (I.map (of f)) (mk f p) :=
by
rw [quotAdjoinRootEquivQuotPolynomialQuot, RingEquiv.symm_trans_apply, RingEquiv.symm_trans_apply,
RingEquiv.symm_trans_apply, RingEquiv.symm_symm, Polynomial.quotQuotEquivComm_mk, Ideal.quotEquivOfEq_symm,
Ideal.quotEquivOfEq_mk, ← RingHom.comp_apply, ← DoubleQuot.quotQuotMk,
quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_symm_quotQuotMk, quotMapOfEquivQuotMapCMapSpanMk_symm_mk]
