Theorems · Definition · ring theory

NonUnitalRingHom.eqLocus

{R : Type u} →
  {S : Type v} →
    [inst : NonUnitalNonAssocRing R] → [inst_1 : NonUnitalNonAssocRing S] → (R →ₙ+* S) → (R →ₙ+* S) → NonUnitalSubring R

The NonUnitalSubring of elements x : R such that f x = g x, i.e., the equalizer of f and g as a NonUnitalSubring of R

Defined in

Mathlib.RingTheory.NonUnitalSubring.Basic

Cited by

3 results in Mathlib

Foundations

Depth 16 from the axioms · uses propext

Assumes

NonUnitalNonAssocRingNonUnitalNonAssocRing