eqLocus — Mathlib

English

The equalizer of two ring homomorphisms f,g: R →+* S is the subring of R consisting of elements x with f(x) = g(x).

Русский

Равносравнение двух гомоморфизмов f,g: R →+* S — это подкольцо R, состоящее из элементов x с f(x) = g(x).

LaTeX

$$$ \\operatorname{eqLocus}(f,g) = \\{ x \\in R \\mid f(x) = g(x) \\} $$$

Lean4

/-- 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 -/
def eqLocus (f g : R →+* S) : Subring R :=
  { (f : R →* S).eqLocusM g, (f : R →+ S).eqLocus g with carrier := {x | f x = g x} }

Похожие утверждения