English
Given an equivalence e: α ≃ β, there is a multiplicative equivalence FreeGroup α ≃* FreeGroup β extending e.
Русский
Для эквивалентности e: α ≃ β существует мультипликативное эквивалентность FreeGroup α ≃* FreeGroup β, которая расширяет e на генераторах.
LaTeX
$$$ freeGroupCongr\\ (e) : FreeGroup\\ α \\simeq_* FreeGroup\\ β $$$
Lean4
/-- Equivalent types give rise to multiplicatively equivalent free groups.
The converse can be found in `Mathlib/GroupTheory/FreeGroup/GeneratorEquiv.lean`, as
`Equiv.ofFreeGroupEquiv`. -/
@[to_additive (attr := simps apply) /-- Equivalent types give rise to additively equivalent additive free groups. -/
]
def freeGroupCongr {α β} (e : α ≃ β) : FreeGroup α ≃* FreeGroup β
where
toFun := map e
invFun := map e.symm
left_inv x := by simp [map.comp]
right_inv x := by simp [map.comp]
map_mul' := MonoidHom.map_mul _
