eqLocus — Mathlib

English

The set of elements x in G such that f(x) = g(x) forms a subgroup of G.

Русский

Множество элементов x в G, для которых f(x) = g(x), образует подгруппу G.

LaTeX

$$$\operatorname{eqLocus}(f,g) ≤ G$ with $f(x)=g(x)$ for all x$$

Lean4

/-- The subgroup of elements `x : G` such that `f x = g x` -/
@[to_additive /-- The additive subgroup of elements `x : G` such that `f x = g x` -/
    ]
def eqLocus (f g : G →* M) : Subgroup G :=
  { eqLocusM f g with inv_mem' := eq_on_inv f g }

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