English
For hx and h_alg, applying quotAdjoinEquivQuotMap to a canonical quotient element mk(I.map(algebraMap R R<x>)) a yields mk(I.map(algebraMap R S)) ↑a.
Русский
При hx и h_alg применение quotAdjoinEquivQuotMap к каноническому элементу mk(I.map(algebraMap R R<x>)) a даёт mk(I.map(algebraMap R S)) ↑a.
LaTeX
$$$\\text{quotAdjoinEquivQuotMap}(hx,h\\_alg)(\\mathrm{Ideal.Quotient.mk}(I.map(\\mathrm{algebraMap} \\ R \\langle x\\rangle), a)) = \\mathrm{Ideal.Quotient.mk}(I.map(\\mathrm{algebraMap} \\ R S)) (a.1)$$$
Lean4
@[simp]
theorem quotAdjoinEquivQuotMap_apply_mk (hx : (conductor R x).comap (algebraMap R S) ⊔ I = ⊤)
(h_alg : Function.Injective (algebraMap R<x> S)) (a : R<x>) :
quotAdjoinEquivQuotMap hx h_alg (Ideal.Quotient.mk (I.map (algebraMap R R<x>)) a) =
Ideal.Quotient.mk (I.map (algebraMap R S)) ↑a :=
rfl
