eqLocusField — Mathlib

English

The equalizer of f and g as a subfield of K is the set of x with f(x) = g(x).

Русский

Выравнивающее множество (равенство) функций f и g как подполе K состоит из элементов x, для которых f(x) = g(x).

LaTeX

$$$\operatorname{eqLocusField}(f,g) = \{ x \in K \mid f(x) = g(x) \}$$$

Lean4

/-- The subfield of elements `x : R` such that `f x = g x`, i.e.,
the equalizer of f and g as a subfield of R -/
def eqLocusField (f g : K →+* L) : Subfield K
    where
  __ := (f : K →+* L).eqLocus g
  inv_mem' _ := eq_on_inv₀ f g
  carrier := {x | f x = g x}

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