idealQuotientToRingQuot_apply — Mathlib

English

The universal ring homomorphism from B/Ideal.ofRel r to RingQuot r is given by lifting mkRingHom r along Ideal.Quotient.mk.

Русский

Универсальное кольцевое гомоморфизм от B/Ideal.ofRel r к RingQuot r задаётся подъёмом mkRingHom r вдоль Ideal.Quotient.mk.

LaTeX

$$$\\text{idealQuotientToRingQuot} : B/\\!Ideal.ofRel r \\to\\!\\text{RingQuot} r = \\operatorname{Ideal.Quotient.lift}(\\operatorname{Ideal.ofRel r}, mkRingHom r)$$$

Lean4

@[simp]
theorem idealQuotientToRingQuot_apply (r : B → B → Prop) (x : B) :
    idealQuotientToRingQuot r (Ideal.Quotient.mk _ x) = mkRingHom r x :=
  rfl

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