English
There is a natural isomorphism between (R/I)[X] quotiented by the span of f.map (I) and R[X] quotiented by I.map C, quotiented further by f.
Русский
Существует естественный изоморфизм между (R/I)[X] /(span {f.map I}) и R[X]/(I.map C) /(span {f})
LaTeX
$$$\text{quotQuotEquivComm}: (R/I)[X] / \operatorname{span}\{f.map (I)\} \cong+* R[X] /(I.map C) / \operatorname{span}\{(I.map C)\,f\}$$$
Lean4
/-- The natural isomorphism `R[α]/(I[α]) ≅ R[α]/((I[x] ⊔ (f)) / (f))` for `α` a root of
`f : R[X]` and `I : Ideal R`.
See `adjoin_root.quot_map_of_equiv` for the isomorphism with `(R/I)[X] / (f mod I)`. -/
def quotMapOfEquivQuotMapCMapSpanMk :
AdjoinRoot f ⧸ I.map (of f) ≃+* AdjoinRoot f ⧸ (I.map (C : R →+* R[X])).map (Ideal.Quotient.mk (span { f })) :=
Ideal.quotEquivOfEq (by rw [of, AdjoinRoot.mk, Ideal.map_map])
