ringQuotEquivIdealQuotient — Mathlib

English

For all b, ringQuotToIdealQuotient r (Ideal.Quotient.mk (Ideal.ofRel r) b) = mkRingHom r b.

Русский

Для любого b: ringQuotToIdealQuotient r (Ideal.Quotient.mk (Ideal.ofRel r) b) = mkRingHom r b.

LaTeX

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

Lean4

/-- The ring equivalence between `RingQuot r` and `(Ideal.ofRel r).quotient`
-/
def ringQuotEquivIdealQuotient (r : B → B → Prop) : RingQuot r ≃+* B ⧸ Ideal.ofRel r :=
  RingEquiv.ofHomInv (ringQuotToIdealQuotient r) (idealQuotientToRingQuot r)
    (by
      ext x
      simp)
    (by
      ext x
      simp)

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