English
An equivalence e : α ≃ β induces an equivalence between Sym α n and Sym β n.
Русский
Эквивалентность e : α ≃ β индуцирует эквивалентность между Sym α n и Sym β n.
LaTeX
$$$\\forall e : \\alpha \\simeq \\beta,\\ \\mathrm{Sym}(\\alpha,n) \\simeq \\mathrm{Sym}(\\beta,n).$$$
Lean4
/-- Mapping an equivalence `α ≃ β` using `Sym.map` gives an equivalence between `Sym α n` and
`Sym β n`. -/
@[simps]
def equivCongr (e : α ≃ β) : Sym α n ≃ Sym β n where
toFun := map e
invFun := map e.symm
left_inv x := by rw [map_map, Equiv.symm_comp_self, map_id]
right_inv x := by rw [map_map, Equiv.self_comp_symm, map_id]
