unique — Mathlib

English

Evaluating the equivalence-preserving map on generators matches the corresponding mapped generator.

Русский

Применение эквивалентного отображения к образу генератора совпадает с образом соответствующего элемента.

LaTeX

$$equivPresentedGroup rels e (PresentedGroup.of x) = PresentedGroup.of (e x)$$

Lean4

theorem unique (h : ∀ r ∈ rels, FreeGroup.lift f r = 1) (g : PresentedGroup rels →* G)
    (hg : ∀ x : α, g (PresentedGroup.of x) = f x) : ∀ {x}, g x = toGroup h x :=
  by
  intro x
  refine QuotientGroup.induction_on x ?_
  exact fun _ ↦ FreeGroup.lift_unique (g.comp (QuotientGroup.mk' _)) hg

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