English
There is a canonical RingQuot r →+* B/Ideal.ofRel r, obtained by lifting the quotient map to the ideal quotient.
Русский
Существует каноническое отображение RingQuot r →+* B/Ideal.ofRel r, полученное посредством подъёма отображения квартизирования в фактор по идеалу.
LaTeX
$$$\\text{ringQuotToIdealQuotient} : RingQuot r \\to+* (B\\/Ideal.ofRel r) = \\operatorname{lift}(\\langle \\operatorname{Ideal.Quotient.mk}(\\operatorname{Ideal.ofRel r}), \\dots \\rangle)$$$
Lean4
@[simp]
theorem lift_mkRingHom_apply (f : R →+* T) {r : R → R → Prop} (w : ∀ ⦃x y⦄, r x y → f x = f y) (x) :
lift ⟨f, w⟩ (mkRingHom r x) = f x :=
by
simp_rw [lift_def, preLift_def, mkRingHom_def]
rfl
-- note this is essentially `lift.symm_apply_eq.mp h`
