mem_eqLocus — Mathlib

English

For ring homomorphisms f,g: R →+* S and x ∈ R, x is in eqLocus(f,g) if and only if f(x) = g(x).

Русский

Для гомоморфизмов колец f,g: R →+* S и элемента x ∈ R: x принадлежит eqLocus(f,g) тогда и только тогда, когда f(x) = g(x).

LaTeX

$$$ x \\in f.\\mathrm{eqLocus}(g) \\iff f(x) = g(x) $$$

Lean4

@[simp]
theorem mem_eqLocus {f g : R →+* S} {x : R} : x ∈ f.eqLocus g ↔ f x = g x :=
  Iff.rfl

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