equivPresentedGroup_apply_of — Mathlib

English

Applying an equivalence-preserving map to generators corresponds to mapping generators under the induced equivalence.

Русский

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

LaTeX

$$equivPresentedGroup_apply_of (x : α) (rels : Set (FreeGroup α)) (e : α ≃ β) : equivPresentedGroup rels e (PresentedGroup.of x) = PresentedGroup.of (rels := FreeGroup.freeGroupCongr e '' rels) (e x)$$

Lean4

theorem equivPresentedGroup_apply_of (x : α) (rels : Set (FreeGroup α)) (e : α ≃ β) :
    equivPresentedGroup rels e (PresentedGroup.of x) =
      PresentedGroup.of (rels := FreeGroup.freeGroupCongr e '' rels) (e x) :=
  rfl

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