to_group_eq_one_of_mem_closure — Mathlib

English

Equality mk rels x = 1 is equivalent to x belonging to the normal closure of rels.

Русский

Равенство mk rels x = 1 эквивалентно тому, что x принадлежит нормальному замыканию rels.

LaTeX

$$$mk(\mathrm{rels}, x) = 1 \iff x \in \operatorname{normalClosure}(\mathrm{rels})$$$

Lean4

theorem to_group_eq_one_of_mem_closure (h : ∀ r ∈ rels, FreeGroup.lift f r = 1) :
    ∀ x ∈ Subgroup.normalClosure rels, F x = 1 := fun _ w ↦ MonoidHom.mem_ker.1 <| closure_rels_subset_ker h w

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