Theorems · Definition · commutative algebra

Ideal.Quotient.mk

{R : Type u} → [inst : Ring R] → (I : Ideal R) → [inst_1 : I.IsTwoSided] → R →+* R ⧸ I

The ring homomorphism from a ring R to a quotient ring R/I.

Defined in

Mathlib.RingTheory.Ideal.Quotient.Defs

Cited by

610 results in Mathlib

Foundations

Depth 82 from the axioms, rests on 1,317 definitions · uses propext, Classical.choice, Quot.sound

Assumes

RingIdeal.IsTwoSided