Theorems · Definition · commutative algebra

RingCon.mapGen

{M : Type u_1} →
  {N : Type u_2} → [inst : NonAssocSemiring M] → [inst_1 : NonAssocSemiring N] → {c : RingCon M} → (M → N) → RingCon N

Given a function f, the smallest ring congruence relation containing the binary relation on f's image defined by 'x ≈ y iff the elements of f⁻¹(x) are related to the elements of f⁻¹(y) by a ring congruence relation c.'

Defined in

Mathlib.RingTheory.Congruence.Hom

Cited by

2 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms

Assumes

NonAssocSemiringNonAssocSemiring