equivPresentedGroup_symm_apply_of

English

The inverse equivalence maps the canonical generator back to its image under the inverse of the original equivalence.

Русский

Обратное изоморфизм отображает канонический генератор в образ через обратное соответствие.

LaTeX

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

Lean4

theorem equivPresentedGroup_symm_apply_of (x : β) (rels : Set (FreeGroup α)) (e : α ≃ β) :
    (equivPresentedGroup rels e).symm (PresentedGroup.of x) = PresentedGroup.of (rels := rels) (e.symm x) :=
  rfl

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