Theorems · Definition · commutative algebra

RingCon.map

{M : Type u_1} → [inst : NonAssocSemiring M] → (c d : RingCon M) → c ≤ d → c.Quotient →+* d.Quotient

Given ring congruence relations c, d on a ring such that d contains c, d's quotient map induces a homomorphism from the quotient by c to the quotient by d.

Defined in

Mathlib.RingTheory.Congruence.Hom

Cited by

4 results in Mathlib

Foundations

Depth 34 from the axioms · uses propext, Quot.sound

Assumes

NonAssocSemiring