Theorems · Definition · commutative algebra

RingHom.eqLocus

{R : Type u} → [inst : NonAssocRing R] → {S : Type v} → [inst_1 : Semiring S] → (R →+* S) → (R →+* S) → Subring R

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

Defined in

Mathlib.Algebra.Ring.Subring.Basic

Cited by

12 results in Mathlib

Foundations

Depth 19 from the axioms · uses propext

Assumes

NonAssocRingSemiring