ringQuotToIdealQuotient — Mathlib

English

The application of ringQuotToIdealQuotient to mkRingHom r x yields the canonical quotient element of x modulo Ideal.ofRel r.

Русский

Применение ringQuotToIdealQuotient к mkRingHom r x даёт канонический класс x по модулю Ideал.ofRel r.

LaTeX

$$$ringQuotToIdealQuotient\\ r\\ (mkRingHom\\ r\\ x) =\\ Ideal.Quotient.mk\\ (Ideal.ofRel r)\\ x$$$

Lean4

/-- The universal ring homomorphism from `RingQuot r` to `B ⧸ Ideal.ofRel r`. -/
def ringQuotToIdealQuotient (r : B → B → Prop) : RingQuot r →+* B ⧸ Ideal.ofRel r :=
  lift
    ⟨Ideal.Quotient.mk (Ideal.ofRel r), fun x y h ↦
      Ideal.Quotient.eq.2 <| Submodule.mem_sInf.mpr fun _ w ↦ w ⟨x, y, h, sub_add_cancel x y⟩⟩

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